:: ALGSEQ_1 semantic presentation

definition

let c₁ be Nat;
func PSeg a₁ -> set equals :: ALGSEQ_1:def 1
{ b₁ where B is Nat : b₁ < a₁ } ;
coherence ;

end;

:: deftheorem defines PSeg ALGSEQ_1:def 1 :

definition

let c₁ be Nat;
redefine func PSeg as PSeg a₁ -> Subset of NAT ;
coherence

proof

set c₂ = PSeg c₁;
PSeg c₁ c= NAT

proof

let c₃ be set ; :: uses TARSKI:def 3
assume c₃ in PSeg c₁ ;
then c₃ in { b₁ where B is Nat : b₁ < c₁ } ;
then ( ex b₁ being Nat st
( c₃ = b₁ & b₁ < c₁ ) & ex b₁ being set st b₁ in NAT ) ;
hence c₃ in NAT ;

end;

hence PSeg c₁ is Subset of NAT ;

end;

E1: for b₁ being Nat
for b₂ being set holds
( b₂ in PSeg b₁ implies b₂ is Nat )
;

theorem :: ALGSEQ_1:1

canceled;

theorem :: ALGSEQ_1:2

canceled;

theorem :: ALGSEQ_1:3

canceled;

theorem :: ALGSEQ_1:4

canceled;

theorem :: ALGSEQ_1:5

canceled;

theorem :: ALGSEQ_1:6

canceled;

theorem :: ALGSEQ_1:7

canceled;

theorem :: ALGSEQ_1:8

canceled;

theorem :: ALGSEQ_1:9

canceled;

theorem E2: :: ALGSEQ_1:10

for b₁, b₂ being Nat holds
( b₁ in PSeg b₂ iff b₁ < b₂ )

proof

let c₁, c₂ be Nat;
( c₁ in { b₁ where B is Nat : b₁ < c₂ } iff ex b₁ being Nat st
( c₁ = b₁ & b₁ < c₂ ) ) ;
hence ( c₁ in PSeg c₂ iff c₁ < c₂ ) ;

end;

theorem E3: :: ALGSEQ_1:11

( PSeg 0 = {} & PSeg 1 = {0} & PSeg 2 = {0,1} )

proof

hereby

assume E4: PSeg 0 <> {} ;
consider c₁ being Element of PSeg 0;
reconsider c₂ = c₁ as Nat by E4, E1;
c₂ < 0 by E4, E2;
hence not verum by NAT_1:18;

end;

now

let c₁ be set ;
thus ( c₁ in PSeg 1 implies c₁ in {0} )

proof

assume E4: c₁ in PSeg 1 ;
PSeg 1 = { b₁ where B is Nat : b₁ < 1 } ;
then consider c₂ being Nat such that
E5: ( c₁ = c₂ & c₂ < 1 ) by E4;
c₂ < 0 + 1 by E5;
then c₂ <= 0 by NAT_1:38;
then c₂ = 0 by NAT_1:18;
hence c₁ in {0} by E5, TARSKI:def 1;

end;

assume c₁ in {0} ;
then E4: c₁ = 0 by TARSKI:def 1;
0 in { b₁ where B is Nat : b₁ < 1 } ;
hence c₁ in PSeg 1 by E4;

end;

hence PSeg 1 = {0} by TARSKI:2;

now

let c₁ be set ;
thus ( c₁ in PSeg 2 implies c₁ in {0,1} )

proof

assume E4: c₁ in PSeg 2 ;
PSeg 2 = { b₁ where B is Nat : b₁ < 2 } ;
then consider c₂ being Nat such that
E5: ( c₁ = c₂ & c₂ < 2 ) by E4;
( c₂ = 0 or c₂ = 1 ) by E5, NAT_1:71;
hence c₁ in {0,1} by E5, TARSKI:def 2;

end;

assume c₁ in {0,1} ;
then ( c₁ = 0 or c₁ = 1 ) by TARSKI:def 2;
then c₁ in { b₁ where B is Nat : b₁ < 2 } ;
hence c₁ in PSeg 2 ;

end;

hence PSeg 2 = {0,1} by TARSKI:2;

end;

theorem E4: :: ALGSEQ_1:12

for b₁ being Nat holds b₁ in PSeg (b₁ + 1)

proof

let c₁ be Nat;
c₁ < c₁ + 1 by XREAL_1:31;
then c₁ in { b₁ where B is Nat : b₁ < c₁ + 1 } ;
hence c₁ in PSeg (c₁ + 1) ;

end;

theorem E5: :: ALGSEQ_1:13

for b₁, b₂ being Nat holds
( b₁ <= b₂ iff PSeg b₁ c= PSeg b₂ )

proof

let c₁, c₂ be Nat;
thus ( c₁ <= c₂ implies PSeg c₁ c= PSeg c₂ )

proof

assume E6: c₁ <= c₂ ;
let c₃ be set ; :: uses TARSKI:def 3
assume E7: c₃ in PSeg c₁ ;
then reconsider c₄ = c₃ as Nat ;
c₄ < c₁ by E7, E2;
then c₄ < c₂ by E6, XREAL_1:2;
then c₃ in { b₁ where B is Nat : b₁ < c₂ } ;
hence c₃ in PSeg c₂ ;

end;

now

assume not c₁ <= c₂ ;
then c₂ in PSeg c₁ ;
hence ( PSeg c₁ c= PSeg c₂ implies c₁ <= c₂ ) by E2;

end;

hence ( PSeg c₁ c= PSeg c₂ implies c₁ <= c₂ ) ;

end;

theorem E6: :: ALGSEQ_1:14

for b₁, b₂ being Nat holds
( PSeg b₁ = PSeg b₂ implies b₁ = b₂ )

proof

let c₁, c₂ be Nat;
assume PSeg c₁ = PSeg c₂ ;
then ( c₁ <= c₂ & c₂ <= c₁ ) by E5;
hence c₁ = c₂ by XREAL_1:1;

end;

theorem E7: :: ALGSEQ_1:15

for b₁, b₂ being Nat holds
( b₁ <= b₂ implies ( PSeg b₁ = (PSeg b₁) /\ (PSeg b₂) & PSeg b₁ = (PSeg b₂) /\ (PSeg b₁) ) )

proof

let c₁, c₂ be Nat;
assume c₁ <= c₂ ;
then PSeg c₁ c= PSeg c₂ by E5;
hence ( PSeg c₁ = (PSeg c₁) /\ (PSeg c₂) & PSeg c₁ = (PSeg c₂) /\ (PSeg c₁) ) by XBOOLE_1:28;

end;

theorem :: ALGSEQ_1:16

for b₁, b₂ being Nat holds
( ( PSeg b₁ = (PSeg b₁) /\ (PSeg b₂) or PSeg b₁ = (PSeg b₂) /\ (PSeg b₁) ) implies b₁ <= b₂ )

proof

let c₁, c₂ be Nat;

now

assume E8: PSeg c₁ = (PSeg c₁) /\ (PSeg c₂) ;
assume not c₁ <= c₂ ;
then PSeg c₂ = PSeg c₁ by E8, E7;
hence c₁ <= c₂ by E6;

end;

hence ( ( PSeg c₁ = (PSeg c₁) /\ (PSeg c₂) or PSeg c₁ = (PSeg c₂) /\ (PSeg c₁) ) implies c₁ <= c₂ ) ;

end;

theorem :: ALGSEQ_1:17

for b₁ being Nat holds (PSeg b₁) \/ {b₁} = PSeg (b₁ + 1)

proof

let c₁ be Nat;
thus (PSeg c₁) \/ {c₁} c= PSeg (c₁ + 1) :: uses XBOOLE_0:def 10

proof

c₁ + 0 <= c₁ + 1 by XREAL_1:9;
then E8: PSeg c₁ c= PSeg (c₁ + 1) by E5;
let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in (PSeg c₁) \/ {c₁} ;
then ( c₂ in PSeg c₁ or c₂ in {c₁} ) by XBOOLE_0:def 2;
then ( c₂ in PSeg (c₁ + 1) or c₂ = c₁ ) by E8, TARSKI:def 1;
hence c₂ in PSeg (c₁ + 1) by E4;

end;

let c₂ be set ; :: uses TARSKI:def 3
assume E8: c₂ in PSeg (c₁ + 1) ;
then reconsider c₃ = c₂ as Nat ;
c₃ < c₁ + 1 by E8, E2;
then not ( not c₃ < c₁ & not c₃ = c₁ ) by NAT_1:70;
then ( c₃ in PSeg c₁ or c₃ in {c₁} ) by TARSKI:def 1;
hence c₂ in (PSeg c₁) \/ {c₁} by XBOOLE_0:def 2;

end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be sequence of c₁;
attr a₂ is finite-Support means :E8: :: ALGSEQ_1:def 2
ex b₁ being Nat st
for b₂ being Nat holds
( b₂ >= b₁ implies a₂ . b₂ = 0. a₁ );

end;

:: deftheorem E8 defines finite-Support ALGSEQ_1:def 2 :

registration

let c₁ be non empty ZeroStr ;
cluster finite-Support M5( NAT ,the carrier of a₁);
existence

proof

set c₂ = NAT --> (0. c₁);
E9: for b₁ being set holds
( b₁ in NAT implies (NAT --> (0. c₁)) . b₁ = 0. c₁ ) by FUNCOP_1:13;
reconsider c₃ = NAT --> (0. c₁) as Function of NAT ,the carrier of c₁ by FUNCOP_1:57;
take c₃ ;
take 0 ; :: uses ALGSEQ_1:def 2
thus for b₁ being Nat holds
( b₁ >= 0 implies c₃ . b₁ = 0. c₁ ) by E9;

end;

definition

let c₁ be non empty ZeroStr ;
mode AlgSequence is finite-Support sequence of a₁;

end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
let c₃ be Nat;
pred a₃ is_at_least_length_of a₂ means :E9: :: ALGSEQ_1:def 3
for b₁ being Nat holds
( b₁ >= a₃ implies a₂ . b₁ = 0. a₁ );

end;

:: deftheorem E9 defines is_at_least_length_of ALGSEQ_1:def 3 :

E10: for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ holds
ex b₃ being Nat st b₃ is_at_least_length_of b₂

proof

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
consider c₃ being Nat such that
E11: for b₁ being Nat holds
( b₁ >= c₃ implies c₂ . b₁ = 0. c₁ ) by E8;
take c₃ ;
thus c₃ is_at_least_length_of c₂ by E11, E9;

end;

E11: for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ holds
ex b₃ being Nat st
( b₃ is_at_least_length_of b₂ & for b₄ being Nat holds
( b₄ is_at_least_length_of b₂ implies b₃ <= b₄ ) )

proof

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
defpred S₁[ Nat] means a₁ is_at_least_length_of c₂;
E12: ex b₁ being Nat st
S₁[b₁] by E10;
ex b₁ being Nat st
( S₁[b₁] & for b₂ being Nat holds
( S₁[b₂] implies b₁ <= b₂ ) ) from NAT_1:sch 5(E12);
then consider c₃ being Nat such that
E13: ( c₃ is_at_least_length_of c₂ & for b₁ being Nat holds
( b₁ is_at_least_length_of c₂ implies c₃ <= b₁ ) ) ;
take c₃ ;
thus ( c₃ is_at_least_length_of c₂ & for b₁ being Nat holds
( b₁ is_at_least_length_of c₂ implies c₃ <= b₁ ) ) by E13;

end;

E12: for b₁, b₂ being Nat
for b₃ being non empty ZeroStr
for b₄ being AlgSequence of b₃ holds
( ( b₁ is_at_least_length_of b₄ & for b₅ being Nat holds
( b₅ is_at_least_length_of b₄ implies b₁ <= b₅ ) & b₂ is_at_least_length_of b₄ & for b₅ being Nat holds
( b₅ is_at_least_length_of b₄ implies b₂ <= b₅ ) ) implies ( b₁ = b₂ ) )

proof

let c₁, c₂ be Nat;
let c₃ be non empty ZeroStr ;
let c₄ be AlgSequence of c₃;
assume ( c₁ is_at_least_length_of c₄ & for b₁ being Nat holds
( b₁ is_at_least_length_of c₄ implies c₁ <= b₁ ) & c₂ is_at_least_length_of c₄ & for b₁ being Nat holds
( b₁ is_at_least_length_of c₄ implies c₂ <= b₁ ) ) ;
then ( c₁ <= c₂ & c₂ <= c₁ ) ;
hence c₁ = c₂ by XREAL_1:1;

end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
func len a₂ -> Nat means :E13: :: ALGSEQ_1:def 4
( a₃ is_at_least_length_of a₂ & for b₁ being Nat holds
( b₁ is_at_least_length_of a₂ implies a₃ <= b₁ ) );
existence by E11;
uniqueness by E12;

end;

:: deftheorem E13 defines len ALGSEQ_1:def 4 :

theorem :: ALGSEQ_1:18

canceled;

theorem :: ALGSEQ_1:19

canceled;

theorem :: ALGSEQ_1:20

canceled;

theorem :: ALGSEQ_1:21

canceled;

theorem E14: :: ALGSEQ_1:22

for b₁ being Nat
for b₂ being non empty ZeroStr
for b₃ being AlgSequence of b₂ holds
( b₁ >= len b₃ implies b₃ . b₁ = 0. b₂ )

proof

let c₁ be Nat;
let c₂ be non empty ZeroStr ;
let c₃ be AlgSequence of c₂;
assume E15: c₁ >= len c₃ ;
len c₃ is_at_least_length_of c₃ by E13;
hence c₃ . c₁ = 0. c₂ by E15, E9;

end;

theorem :: ALGSEQ_1:23

canceled;

theorem E15: :: ALGSEQ_1:24

for b₁ being Nat
for b₂ being non empty ZeroStr
for b₃ being AlgSequence of b₂ holds
( for b₄ being Nat holds
not ( b₄ < b₁ & not b₃ . b₄ <> 0. b₂ ) implies len b₃ >= b₁ )

proof

let c₁ be Nat;
let c₂ be non empty ZeroStr ;
let c₃ be AlgSequence of c₂;
assume E16: for b₁ being Nat holds
not ( b₁ < c₁ & not c₃ . b₁ <> 0. c₂ ) ;
for b₁ being Nat holds
not ( b₁ < c₁ & not len c₃ > b₁ )

proof

let c₄ be Nat;
assume c₄ < c₁ ;
then c₃ . c₄ <> 0. c₂ by E16;
hence len c₃ > c₄ by E14;

end;

hence len c₃ >= c₁ ;

end;

theorem E16: :: ALGSEQ_1:25

for b₁ being Nat
for b₂ being non empty ZeroStr
for b₃ being AlgSequence of b₂ holds
not ( len b₃ = b₁ + 1 & not b₃ . b₁ <> 0. b₂ )

proof

let c₁ be Nat;
let c₂ be non empty ZeroStr ;
let c₃ be AlgSequence of c₂;
assume E17: len c₃ = c₁ + 1 ;
then c₁ < len c₃ by XREAL_1:31;
then not c₁ is_at_least_length_of c₃ by E13;
then consider c₄ being Nat such that
E18: ( c₄ >= c₁ & c₃ . c₄ <> 0. c₂ ) by E9;
c₄ < c₁ + 1 by E17, E18, E14;
then c₄ <= c₁ by NAT_1:38;
hence c₃ . c₁ <> 0. c₂ by E18, XREAL_1:1;

end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
func support a₂ -> Subset of NAT equals :: ALGSEQ_1:def 5
PSeg (len a₂);
coherence ;

end;

:: deftheorem defines support ALGSEQ_1:def 5 :

theorem :: ALGSEQ_1:26

canceled;

theorem :: ALGSEQ_1:27

for b₁ being Nat
for b₂ being non empty ZeroStr
for b₃ being AlgSequence of b₂ holds
( b₁ = len b₃ iff PSeg b₁ = support b₃ )

proof

let c₁ be Nat;
let c₂ be non empty ZeroStr ;
let c₃ be AlgSequence of c₂;

now

assume PSeg c₁ = support c₃ ;
then PSeg c₁ = PSeg (len c₃) ;
hence c₁ = len c₃ by E6;

end;

hence ( c₁ = len c₃ iff PSeg c₁ = support c₃ ) ;

end;

scheme :: ALGSEQ_1:sch 1
s1{ F₁() -> non empty ZeroStr , F₂() -> Nat, F₃( Nat) -> Element of F₁() } :

ex b₁ being AlgSequence of F₁() st
( len b₁ <= F₂() & for b₂ being Nat holds
( b₂ < F₂() implies b₁ . b₂ = F₃(b₂) ) )

provided

proof

defpred S₁[ Element of NAT , Element of F₁()] means ( ( a₁ < F₂() & a₂ = F₃(a₁) ) or ( a₁ >= F₂() & a₂ = 0. F₁() ) );
E17: for b₁ being Element of NAT holds
ex b₂ being Element of F₁() st
S₁[b₁,b₂]

proof

let c₁ be Element of NAT ;
( c₁ < F₂() implies ( c₁ < F₂() & F₃(c₁) = F₃(c₁) ) ) ;
hence ex b₁ being Element of F₁() st
S₁[c₁,b₁] ;

end;

ex b₁ being Function of NAT ,the carrier of F₁() st
for b₂ being Element of NAT holds
S₁[b₂,b₁ . b₂] from FUNCT_2:sch 3(E17);
then consider c₁ being Function of NAT ,the carrier of F₁() such that
E18: for b₁ being Element of NAT holds
( ( b₁ < F₂() & c₁ . b₁ = F₃(b₁) ) or ( b₁ >= F₂() & c₁ . b₁ = 0. F₁() ) ) ;
ex b₁ being Nat st
for b₂ being Nat holds
( b₂ >= b₁ implies c₁ . b₂ = 0. F₁() )

proof

take F₂() ;
thus for b₁ being Nat holds
( b₁ >= F₂() implies c₁ . b₁ = 0. F₁() ) by E18;

end;

then reconsider c₂ = c₁ as AlgSequence of F₁() by E8;
E19: len c₂ <= F₂()

proof

for b₁ being Nat holds
( b₁ >= F₂() implies c₂ . b₁ = 0. F₁() ) by E18;
then F₂() is_at_least_length_of c₂ by E9;
hence len c₂ <= F₂() by E13;

end;

take c₂ ;
thus ( len c₂ <= F₂() & for b₁ being Nat holds
( b₁ < F₂() implies c₂ . b₁ = F₃(b₁) ) ) by E18, E19;

end;

theorem E17: :: ALGSEQ_1:28

for b₁ being non empty ZeroStr
for b₂, b₃ being AlgSequence of b₁ holds
( ( len b₂ = len b₃ & for b₄ being Nat holds
( b₄ < len b₂ implies b₂ . b₄ = b₃ . b₄ ) ) implies ( b₂ = b₃ ) )

proof

let c₁ be non empty ZeroStr ;
let c₂, c₃ be AlgSequence of c₁;
assume E18: ( len c₂ = len c₃ & for b₁ being Nat holds
( b₁ < len c₂ implies c₂ . b₁ = c₃ . b₁ ) ) ;
E19: ( dom c₂ = NAT & dom c₃ = NAT ) by FUNCT_2:def 1;
for b₁ being set holds
( b₁ in NAT implies c₂ . b₁ = c₃ . b₁ )

proof

let c₄ be set ;
assume c₄ in NAT ;
then reconsider c₅ = c₄ as Nat ;
c₂ . c₅ = c₃ . c₅

proof

( c₅ >= len c₂ implies c₂ . c₅ = c₃ . c₅ )

proof

assume c₅ >= len c₂ ;
then ( c₂ . c₅ = 0. c₁ & c₃ . c₅ = 0. c₁ ) by E18, E14;
hence c₂ . c₅ = c₃ . c₅ ;

end;

hence c₂ . c₅ = c₃ . c₅ by E18;

end;

hence c₂ . c₄ = c₃ . c₄ ;

end;

hence c₂ = c₃ by E19, FUNCT_1:9;

end;

theorem :: ALGSEQ_1:29

for b₁ being non empty ZeroStr holds
( the carrier of b₁ <> {(0. b₁)} implies for b₂ being Nat holds
ex b₃ being AlgSequence of b₁ st len b₃ = b₂ )

proof

let c₁ be non empty ZeroStr ;
set c₂ = the carrier of c₁;
assume E18: the carrier of c₁ <> {(0. c₁)} ;
let c₃ be Nat;
consider c₄ being set such that
E19: ( c₄ in the carrier of c₁ & c₄ <> 0. c₁ ) by E18, ZFMISC_1:41;
reconsider c₅ = c₄ as Element of c₁ by E19;
deffunc H₁( Element of NAT ) -> Element of c₁ = c₅;
consider c₆ being AlgSequence of c₁ such that
E20: ( len c₆ <= c₃ & for b₁ being Nat holds
( b₁ < c₃ implies c₆ . b₁ = H₁(b₁) ) ) from ALGSEQ_1:sch 1();
for b₁ being Nat holds
not ( b₁ < c₃ & not c₆ . b₁ <> 0. c₁ ) by E19, E20;
then len c₆ >= c₃ by E15;
then len c₆ = c₃ by E20, XREAL_1:1;
hence ex b₁ being AlgSequence of c₁ st len b₁ = c₃ ;

end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be Element of c₁;
func <%a₂%> -> AlgSequence of a₁ means :E18: :: ALGSEQ_1:def 6
( len a₃ <= 1 & a₃ . 0 = a₂ );
existence

proof

deffunc H₁( Element of NAT ) -> Element of c₁ = c₂;
consider c₃ being AlgSequence of c₁ such that
E18: ( len c₃ <= 1 & for b₁ being Nat holds
( b₁ < 1 implies c₃ . b₁ = H₁(b₁) ) ) from ALGSEQ_1:sch 1();
take c₃ ;
thus ( len c₃ <= 1 & c₃ . 0 = c₂ ) by E18;

end;

uniqueness

proof

let c₃, c₄ be AlgSequence of c₁;
assume that E18: ( len c₃ <= 1 & c₃ . 0 = c₂ )
and E19: ( len c₄ <= 1 & c₄ . 0 = c₂ ) ;
E20: 1 = 0 + 1 ;

E21: now

assume c₂ = 0. c₁ ;
then ( len c₃ <> 1 & len c₄ <> 1 ) by E18, E19, E20, E16;
then ( len c₃ < 1 & len c₄ < 1 ) by E18, E19, REAL_1:def 5;
then ( len c₃ = 0 & len c₄ = 0 ) by NAT_1:39;
hence len c₃ = len c₄ ;

end;

E22: now

assume c₂ <> 0. c₁ ;
then ( len c₃ > 0 & len c₄ > 0 ) by E18, E19, E14;
then ( len c₃ = 1 & len c₄ = 1 ) by E18, E19, E20, NAT_1:26;
hence len c₃ = len c₄ ;

end;

for b₁ being Nat holds
( b₁ < len c₃ implies c₃ . b₁ = c₄ . b₁ )

proof

let c₅ be Nat;
assume c₅ < len c₃ ;
then c₅ < 1 by E18, XREAL_1:2;
then c₅ = 0 by NAT_1:39;
hence c₃ . c₅ = c₄ . c₅ by E18, E19;

end;

hence c₃ = c₄ by E21, E22, E17;

end;

:: deftheorem E18 defines <% ALGSEQ_1:def 6 :

E19: for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ holds
( b₂ = <%(0. b₁)%> implies len b₂ = 0 )

proof

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
E20: 0 + 1 = 1 ;
assume c₂ = <%(0. c₁)%> ;
then ( len c₂ <= 1 & c₂ . 0 = 0. c₁ ) by E18;
then ( len c₂ <= 1 & len c₂ <> 1 ) by E20, E16;
then len c₂ < 1 by REAL_1:def 5;
hence len c₂ = 0 by NAT_1:39;

end;

theorem :: ALGSEQ_1:30

canceled;

theorem E20: :: ALGSEQ_1:31

for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ holds
( b₂ = <%(0. b₁)%> iff len b₂ = 0 )

proof

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
thus ( c₂ = <%(0. c₁)%> implies len c₂ = 0 ) by E19;
thus ( len c₂ = 0 implies c₂ = <%(0. c₁)%> )

proof

assume E21: len c₂ = 0 ;
then E22: len c₂ = len <%(0. c₁)%> by E19;
for b₁ being Nat holds
( b₁ < len c₂ implies c₂ . b₁ = <%(0. c₁)%> . b₁ ) by E21, NAT_1:18;
hence c₂ = <%(0. c₁)%> by E22, E17;

end;

theorem :: ALGSEQ_1:32

for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ holds
( b₂ = <%(0. b₁)%> iff support b₂ = {} )

proof

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
thus ( c₂ = <%(0. c₁)%> implies support c₂ = {} )

proof

assume c₂ = <%(0. c₁)%> ;
then len c₂ = 0 by E19;
hence support c₂ = {} by E3;

end;

assume E21: support c₂ = {} ;
support c₂ = PSeg (len c₂) ;
then len c₂ = 0 by E21, E3, E6;
hence c₂ = <%(0. c₁)%> by E20;

end;

theorem E21: :: ALGSEQ_1:33

for b₁ being Nat
for b₂ being non empty ZeroStr holds <%(0. b₂)%> . b₁ = 0. b₂

proof

let c₁ be Nat;
let c₂ be non empty ZeroStr ;
set c₃ = <%(0. c₂)%>;

now

assume c₁ <> 0 ;
then c₁ > 0 by NAT_1:19;
then c₁ >= len <%(0. c₂)%> by E20;
hence <%(0. c₂)%> . c₁ = 0. c₂ by E14;

end;

hence <%(0. c₂)%> . c₁ = 0. c₂ by E18;

end;

theorem :: ALGSEQ_1:34

for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ holds
( b₂ = <%(0. b₁)%> iff rng b₂ = {(0. b₁)} )

proof

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
thus ( c₂ = <%(0. c₁)%> implies rng c₂ = {(0. c₁)} )

proof

assume E22: c₂ = <%(0. c₁)%> ;
thus rng c₂ c= {(0. c₁)} :: uses XBOOLE_0:def 10

proof

let c₃ be set ; :: uses TARSKI:def 3
assume c₃ in rng c₂ ;
then consider c₄ being set such that
E23: ( c₄ in dom c₂ & c₃ = c₂ . c₄ ) by FUNCT_1:def 5;
reconsider c₅ = c₄ as Nat by E23, FUNCT_2:def 1;
c₂ . c₅ = 0. c₁ by E22, E21;
hence c₃ in {(0. c₁)} by E23, TARSKI:def 1;

end;

thus {(0. c₁)} c= rng c₂

proof

let c₃ be set ; :: uses TARSKI:def 3
assume c₃ in {(0. c₁)} ;
then c₃ = 0. c₁ by TARSKI:def 1;
then E23: c₂ . 0 = c₃ by E22, E18;
dom c₂ = NAT by FUNCT_2:def 1;
hence c₃ in rng c₂ by E23, FUNCT_1:def 5;

end;

thus ( rng c₂ = {(0. c₁)} implies c₂ = <%(0. c₁)%> )

proof

assume E22: rng c₂ = {(0. c₁)} ;
len c₂ = 0

proof

for b₁ being Nat holds
( b₁ >= 0 implies c₂ . b₁ = 0. c₁ )

proof

let c₃ be Nat;
c₃ in NAT ;
then c₃ in dom c₂ by FUNCT_2:def 1;
then c₂ . c₃ in rng c₂ by FUNCT_1:def 5;
hence ( c₃ >= 0 implies c₂ . c₃ = 0. c₁ ) by E22, TARSKI:def 1;

end;

then E23: 0 is_at_least_length_of c₂ by E9;
for b₁ being Nat holds
( b₁ is_at_least_length_of c₂ implies 0 <= b₁ ) by NAT_1:18;
hence len c₂ = 0 by E23, E13;

end;

hence c₂ = <%(0. c₁)%> by E20;

end;