:: ALGSEQ_1 semantic presentation begin theorem :: ALGSEQ_1:1 for k, n being Nat holds ( k in Segm n iff k < n ) by NAT_1:44; theorem :: ALGSEQ_1:2 ( Segm 0 = {} & Segm 1 = {0} & Segm 2 = {0,1} ) by CARD_1:49, CARD_1:50; theorem :: ALGSEQ_1:3 for n being Nat holds n in Segm (n + 1) by NAT_1:45; theorem :: ALGSEQ_1:4 for n, m being Nat holds ( n <= m iff Segm n c= Segm m ) by NAT_1:39; theorem :: ALGSEQ_1:5 for n, m being Nat st Segm n = Segm m holds n = m ; theorem :: ALGSEQ_1:6 for k, n being Nat st k <= n holds ( Segm k = (Segm k) /\ (Segm n) & Segm k = (Segm n) /\ (Segm k) ) by NAT_1:46; theorem :: ALGSEQ_1:7 for k, n being Nat st ( Segm k = (Segm k) /\ (Segm n) or Segm k = (Segm n) /\ (Segm k) ) holds k <= n by NAT_1:46; definition let R be non empty ZeroStr ; let F be sequence of R; attrF is finite-Support means :Def1: :: ALGSEQ_1:def 1 ex n being Nat st for i being Nat st i >= n holds F . i = 0. R; end; :: deftheorem Def1 defines finite-Support ALGSEQ_1:def_1_:_ for R being non empty ZeroStr for F being sequence of R holds ( F is finite-Support iff ex n being Nat st for i being Nat st i >= n holds F . i = 0. R ); registration let R be non empty ZeroStr ; cluster Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) finite-Support for Element of K19(K20(NAT, the carrier of R)); existence ex b1 being sequence of R st b1 is finite-Support proof set f = NAT --> (0. R); reconsider f = NAT --> (0. R) as Function of NAT, the carrier of R ; take f ; ::_thesis: f is finite-Support take 0 ; :: according to ALGSEQ_1:def_1 ::_thesis: for i being Nat st i >= 0 holds f . i = 0. R let i be Nat; ::_thesis: ( i >= 0 implies f . i = 0. R ) assume i >= 0 ; ::_thesis: f . i = 0. R i in NAT by ORDINAL1:def_12; hence f . i = 0. R by FUNCOP_1:7; ::_thesis: verum end; end; definition let R be non empty ZeroStr ; mode AlgSequence of R is finite-Support sequence of R; end; definition let R be non empty ZeroStr ; let p be AlgSequence of R; let k be Nat; predk is_at_least_length_of p means :Def2: :: ALGSEQ_1:def 2 for i being Nat st i >= k holds p . i = 0. R; end; :: deftheorem Def2 defines is_at_least_length_of ALGSEQ_1:def_2_:_ for R being non empty ZeroStr for p being AlgSequence of R for k being Nat holds ( k is_at_least_length_of p iff for i being Nat st i >= k holds p . i = 0. R ); Lm1: for R being non empty ZeroStr for p being AlgSequence of R ex m being Nat st m is_at_least_length_of p proof let R be non empty ZeroStr ; ::_thesis: for p being AlgSequence of R ex m being Nat st m is_at_least_length_of p let p be AlgSequence of R; ::_thesis: ex m being Nat st m is_at_least_length_of p consider n being Nat such that A1: for i being Nat st i >= n holds p . i = 0. R by Def1; take n ; ::_thesis: n is_at_least_length_of p thus n is_at_least_length_of p by A1, Def2; ::_thesis: verum end; Lm2: for k, l being Nat for R being non empty ZeroStr for p being AlgSequence of R st k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds l <= m ) holds k = l proof let k, l be Nat; ::_thesis: for R being non empty ZeroStr for p being AlgSequence of R st k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds l <= m ) holds k = l let R be non empty ZeroStr ; ::_thesis: for p being AlgSequence of R st k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds l <= m ) holds k = l let p be AlgSequence of R; ::_thesis: ( k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds l <= m ) implies k = l ) assume ( k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds l <= m ) ) ; ::_thesis: k = l then ( k <= l & l <= k ) ; hence k = l by XXREAL_0:1; ::_thesis: verum end; definition let R be non empty ZeroStr ; let p be AlgSequence of R; func len p -> Element of NAT means :Def3: :: ALGSEQ_1:def 3 ( it is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds it <= m ) ); existence ex b1 being Element of NAT st ( b1 is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds b1 <= m ) ) proof defpred S1[ Nat] means \$1 is_at_least_length_of p; A1: ex m being Nat st S1[m] by Lm1; ex k being Nat st ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A1); then consider k being Nat such that A2: ( k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds k <= n ) ) ; take k ; ::_thesis: ( k is Element of NAT & k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds k <= m ) ) thus ( k is Element of NAT & k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds k <= m ) ) by A2, ORDINAL1:def_12; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st b1 is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds b1 <= m ) & b2 is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds b2 <= m ) holds b1 = b2 by Lm2; end; :: deftheorem Def3 defines len ALGSEQ_1:def_3_:_ for R being non empty ZeroStr for p being AlgSequence of R for b3 being Element of NAT holds ( b3 = len p iff ( b3 is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds b3 <= m ) ) ); theorem Th8: :: ALGSEQ_1:8 for i being Nat for R being non empty ZeroStr for p being AlgSequence of R st i >= len p holds p . i = 0. R proof let i be Nat; ::_thesis: for R being non empty ZeroStr for p being AlgSequence of R st i >= len p holds p . i = 0. R let R be non empty ZeroStr ; ::_thesis: for p being AlgSequence of R st i >= len p holds p . i = 0. R let p be AlgSequence of R; ::_thesis: ( i >= len p implies p . i = 0. R ) assume A1: i >= len p ; ::_thesis: p . i = 0. R len p is_at_least_length_of p by Def3; hence p . i = 0. R by A1, Def2; ::_thesis: verum end; theorem Th9: :: ALGSEQ_1:9 for k being Nat for R being non empty ZeroStr for p being AlgSequence of R st ( for i being Nat st i < k holds p . i <> 0. R ) holds len p >= k proof let k be Nat; ::_thesis: for R being non empty ZeroStr for p being AlgSequence of R st ( for i being Nat st i < k holds p . i <> 0. R ) holds len p >= k let R be non empty ZeroStr ; ::_thesis: for p being AlgSequence of R st ( for i being Nat st i < k holds p . i <> 0. R ) holds len p >= k let p be AlgSequence of R; ::_thesis: ( ( for i being Nat st i < k holds p . i <> 0. R ) implies len p >= k ) assume A1: for i being Nat st i < k holds p . i <> 0. R ; ::_thesis: len p >= k for i being Nat st i < k holds len p > i proof let i be Nat; ::_thesis: ( i < k implies len p > i ) assume i < k ; ::_thesis: len p > i then p . i <> 0. R by A1; hence len p > i by Th8; ::_thesis: verum end; hence len p >= k ; ::_thesis: verum end; theorem Th10: :: ALGSEQ_1:10 for k being Nat for R being non empty ZeroStr for p being AlgSequence of R st len p = k + 1 holds p . k <> 0. R proof let k be Nat; ::_thesis: for R being non empty ZeroStr for p being AlgSequence of R st len p = k + 1 holds p . k <> 0. R let R be non empty ZeroStr ; ::_thesis: for p being AlgSequence of R st len p = k + 1 holds p . k <> 0. R let p be AlgSequence of R; ::_thesis: ( len p = k + 1 implies p . k <> 0. R ) assume A1: len p = k + 1 ; ::_thesis: p . k <> 0. R then k < len p by XREAL_1:29; then not k is_at_least_length_of p by Def3; then consider i being Nat such that A2: i >= k and A3: p . i <> 0. R by Def2; i < k + 1 by A1, A3, Th8; then i <= k by NAT_1:13; hence p . k <> 0. R by A2, A3, XXREAL_0:1; ::_thesis: verum end; definition let R be non empty ZeroStr ; let p be AlgSequence of R; func support p -> Subset of NAT equals :: ALGSEQ_1:def 4 Segm (len p); coherence Segm (len p) is Subset of NAT ; end; :: deftheorem defines support ALGSEQ_1:def_4_:_ for R being non empty ZeroStr for p being AlgSequence of R holds support p = Segm (len p); theorem :: ALGSEQ_1:11 for k being Nat for R being non empty ZeroStr for p being AlgSequence of R holds ( k = len p iff Segm k = support p ) ; scheme :: ALGSEQ_1:sch 1 AlgSeqLambdaF{ F1() -> non empty ZeroStr , F2() -> Nat, F3( Nat) -> Element of F1() } : ex p being AlgSequence of F1() st ( len p <= F2() & ( for k being Nat st k < F2() holds p . k = F3(k) ) ) proof defpred S1[ Nat, Element of F1()] means ( ( \$1 < F2() & \$2 = F3(\$1) ) or ( \$1 >= F2() & \$2 = 0. F1() ) ); A1: for x being Element of NAT ex y being Element of F1() st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of F1() st S1[x,y] ( x < F2() implies ( x < F2() & F3(x) = F3(x) ) ) ; hence ex y being Element of F1() st S1[x,y] ; ::_thesis: verum end; ex f being Function of NAT, the carrier of F1() st for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1); then consider f being Function of NAT, the carrier of F1() such that A2: for x being Element of NAT holds ( ( x < F2() & f . x = F3(x) ) or ( x >= F2() & f . x = 0. F1() ) ) ; ex n being Nat st for i being Nat st i >= n holds f . i = 0. F1() proof reconsider n = F2() as Element of NAT by ORDINAL1:def_12; take n ; ::_thesis: for i being Nat st i >= n holds f . i = 0. F1() let i be Nat; ::_thesis: ( i >= n implies f . i = 0. F1() ) i in NAT by ORDINAL1:def_12; hence ( i >= n implies f . i = 0. F1() ) by A2; ::_thesis: verum end; then reconsider f = f as AlgSequence of F1() by Def1; take f ; ::_thesis: ( len f <= F2() & ( for k being Nat st k < F2() holds f . k = F3(k) ) ) now__::_thesis:_for_i_being_Nat_st_i_>=_F2()_holds_ f_._i_=_0._F1() let i be Nat; ::_thesis: ( i >= F2() implies f . i = 0. F1() ) assume A3: i >= F2() ; ::_thesis: f . i = 0. F1() i in NAT by ORDINAL1:def_12; hence f . i = 0. F1() by A2, A3; ::_thesis: verum end; then F2() is_at_least_length_of f by Def2; hence len f <= F2() by Def3; ::_thesis: for k being Nat st k < F2() holds f . k = F3(k) let k be Nat; ::_thesis: ( k < F2() implies f . k = F3(k) ) k in NAT by ORDINAL1:def_12; hence ( k < F2() implies f . k = F3(k) ) by A2; ::_thesis: verum end; theorem Th12: :: ALGSEQ_1:12 for R being non empty ZeroStr for p, q being AlgSequence of R st len p = len q & ( for k being Nat st k < len p holds p . k = q . k ) holds p = q proof let R be non empty ZeroStr ; ::_thesis: for p, q being AlgSequence of R st len p = len q & ( for k being Nat st k < len p holds p . k = q . k ) holds p = q let p, q be AlgSequence of R; ::_thesis: ( len p = len q & ( for k being Nat st k < len p holds p . k = q . k ) implies p = q ) assume that A1: len p = len q and A2: for k being Nat st k < len p holds p . k = q . k ; ::_thesis: p = q A3: for x being set st x in NAT holds p . x = q . x proof let x be set ; ::_thesis: ( x in NAT implies p . x = q . x ) assume x in NAT ; ::_thesis: p . x = q . x then reconsider k = x as Element of NAT ; ( k >= len p implies p . k = q . k ) proof assume A4: k >= len p ; ::_thesis: p . k = q . k then p . k = 0. R by Th8; hence p . k = q . k by A1, A4, Th8; ::_thesis: verum end; hence p . x = q . x by A2; ::_thesis: verum end; ( dom p = NAT & dom q = NAT ) by FUNCT_2:def_1; hence p = q by A3, FUNCT_1:2; ::_thesis: verum end; theorem :: ALGSEQ_1:13 for R being non empty ZeroStr st the carrier of R <> {(0. R)} holds for k being Nat ex p being AlgSequence of R st len p = k proof let R be non empty ZeroStr ; ::_thesis: ( the carrier of R <> {(0. R)} implies for k being Nat ex p being AlgSequence of R st len p = k ) set D = the carrier of R; assume the carrier of R <> {(0. R)} ; ::_thesis: for k being Nat ex p being AlgSequence of R st len p = k then consider t being set such that A1: t in the carrier of R and A2: t <> 0. R by ZFMISC_1:35; reconsider y = t as Element of R by A1; let k be Nat; ::_thesis: ex p being AlgSequence of R st len p = k deffunc H1( Nat) -> Element of R = y; consider p being AlgSequence of R such that A3: ( len p <= k & ( for i being Nat st i < k holds p . i = H1(i) ) ) from ALGSEQ_1:sch_1(); for i being Nat st i < k holds p . i <> 0. R by A2, A3; then len p >= k by Th9; then len p = k by A3, XXREAL_0:1; hence ex p being AlgSequence of R st len p = k ; ::_thesis: verum end; definition let R be non empty ZeroStr ; let x be Element of R; func<%x%> -> AlgSequence of R means :Def5: :: ALGSEQ_1:def 5 ( len it <= 1 & it . 0 = x ); existence ex b1 being AlgSequence of R st ( len b1 <= 1 & b1 . 0 = x ) proof deffunc H1( Nat) -> Element of R = x; consider p being AlgSequence of R such that A1: ( len p <= 1 & ( for k being Nat st k < 1 holds p . k = H1(k) ) ) from ALGSEQ_1:sch_1(); take p ; ::_thesis: ( len p <= 1 & p . 0 = x ) thus ( len p <= 1 & p . 0 = x ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being AlgSequence of R st len b1 <= 1 & b1 . 0 = x & len b2 <= 1 & b2 . 0 = x holds b1 = b2 proof let p, q be AlgSequence of R; ::_thesis: ( len p <= 1 & p . 0 = x & len q <= 1 & q . 0 = x implies p = q ) assume that A2: len p <= 1 and A3: p . 0 = x and A4: len q <= 1 and A5: q . 0 = x ; ::_thesis: p = q A6: 1 = 0 + 1 ; A7: now__::_thesis:_(_x_=_0._R_implies_len_p_=_len_q_) assume A8: x = 0. R ; ::_thesis: len p = len q then len p < 1 by A2, A3, A6, Th10, XXREAL_0:1; then A9: len p = 0 by NAT_1:14; len q < 1 by A4, A5, A6, A8, Th10, XXREAL_0:1; hence len p = len q by A9, NAT_1:14; ::_thesis: verum end; A10: for k being Nat st k < len p holds p . k = q . k proof let k be Nat; ::_thesis: ( k < len p implies p . k = q . k ) assume k < len p ; ::_thesis: p . k = q . k then k < 1 by A2, XXREAL_0:2; then k = 0 by NAT_1:14; hence p . k = q . k by A3, A5; ::_thesis: verum end; now__::_thesis:_(_x_<>_0._R_implies_len_p_=_len_q_) assume A11: x <> 0. R ; ::_thesis: len p = len q then len p = 1 by A2, A3, A6, Th8, NAT_1:8; hence len p = len q by A4, A5, A6, A11, Th8, NAT_1:8; ::_thesis: verum end; hence p = q by A7, A10, Th12; ::_thesis: verum end; end; :: deftheorem Def5 defines <% ALGSEQ_1:def_5_:_ for R being non empty ZeroStr for x being Element of R for b3 being AlgSequence of R holds ( b3 = <%x%> iff ( len b3 <= 1 & b3 . 0 = x ) ); Lm3: for R being non empty ZeroStr for p being AlgSequence of R st p = <%(0. R)%> holds len p = 0 proof let R be non empty ZeroStr ; ::_thesis: for p being AlgSequence of R st p = <%(0. R)%> holds len p = 0 let p be AlgSequence of R; ::_thesis: ( p = <%(0. R)%> implies len p = 0 ) assume p = <%(0. R)%> ; ::_thesis: len p = 0 then A1: ( p . 0 = 0. R & len p <= 1 ) by Def5; 0 + 1 = 1 ; then len p < 1 by A1, Th10, XXREAL_0:1; hence len p = 0 by NAT_1:14; ::_thesis: verum end; theorem Th14: :: ALGSEQ_1:14 for R being non empty ZeroStr for p being AlgSequence of R holds ( p = <%(0. R)%> iff len p = 0 ) proof let R be non empty ZeroStr ; ::_thesis: for p being AlgSequence of R holds ( p = <%(0. R)%> iff len p = 0 ) let p be AlgSequence of R; ::_thesis: ( p = <%(0. R)%> iff len p = 0 ) thus ( p = <%(0. R)%> implies len p = 0 ) by Lm3; ::_thesis: ( len p = 0 implies p = <%(0. R)%> ) thus ( len p = 0 implies p = <%(0. R)%> ) ::_thesis: verum proof assume len p = 0 ; ::_thesis: p = <%(0. R)%> then ( len p = len <%(0. R)%> & ( for k being Nat st k < len p holds p . k = <%(0. R)%> . k ) ) by Lm3, NAT_1:2; hence p = <%(0. R)%> by Th12; ::_thesis: verum end; end; theorem :: ALGSEQ_1:15 for R being non empty ZeroStr for p being AlgSequence of R holds ( p = <%(0. R)%> iff support p = {} ) by Th14; theorem Th16: :: ALGSEQ_1:16 for i being Nat for R being non empty ZeroStr holds <%(0. R)%> . i = 0. R proof let i be Nat; ::_thesis: for R being non empty ZeroStr holds <%(0. R)%> . i = 0. R let R be non empty ZeroStr ; ::_thesis: <%(0. R)%> . i = 0. R set p0 = <%(0. R)%>; now__::_thesis:_(_i_<>_0_implies_<%(0._R)%>_._i_=_0._R_) assume i <> 0 ; ::_thesis: <%(0. R)%> . i = 0. R then i > 0 by NAT_1:3; then i >= len <%(0. R)%> by Th14; hence <%(0. R)%> . i = 0. R by Th8; ::_thesis: verum end; hence <%(0. R)%> . i = 0. R by Def5; ::_thesis: verum end; theorem :: ALGSEQ_1:17 for R being non empty ZeroStr for p being AlgSequence of R holds ( p = <%(0. R)%> iff rng p = {(0. R)} ) proof let R be non empty ZeroStr ; ::_thesis: for p being AlgSequence of R holds ( p = <%(0. R)%> iff rng p = {(0. R)} ) let p be AlgSequence of R; ::_thesis: ( p = <%(0. R)%> iff rng p = {(0. R)} ) thus ( p = <%(0. R)%> implies rng p = {(0. R)} ) ::_thesis: ( rng p = {(0. R)} implies p = <%(0. R)%> ) proof assume A1: p = <%(0. R)%> ; ::_thesis: rng p = {(0. R)} thus rng p c= {(0. R)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. R)} c= rng p proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in {(0. R)} ) assume x in rng p ; ::_thesis: x in {(0. R)} then consider i being set such that A2: i in dom p and A3: x = p . i by FUNCT_1:def_3; reconsider i = i as Element of NAT by A2, FUNCT_2:def_1; p . i = 0. R by A1, Th16; hence x in {(0. R)} by A3, TARSKI:def_1; ::_thesis: verum end; thus {(0. R)} c= rng p ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. R)} or x in rng p ) assume x in {(0. R)} ; ::_thesis: x in rng p then x = 0. R by TARSKI:def_1; then A4: p . 0 = x by A1, Def5; dom p = NAT by FUNCT_2:def_1; hence x in rng p by A4, FUNCT_1:def_3; ::_thesis: verum end; end; thus ( rng p = {(0. R)} implies p = <%(0. R)%> ) ::_thesis: verum proof assume A5: rng p = {(0. R)} ; ::_thesis: p = <%(0. R)%> for k being Nat st k >= 0 holds p . k = 0. R proof let k be Nat; ::_thesis: ( k >= 0 implies p . k = 0. R ) k in NAT by ORDINAL1:def_12; then k in dom p by FUNCT_2:def_1; then p . k in rng p by FUNCT_1:def_3; hence ( k >= 0 implies p . k = 0. R ) by A5, TARSKI:def_1; ::_thesis: verum end; then A6: 0 is_at_least_length_of p by Def2; for m being Nat st m is_at_least_length_of p holds 0 <= m by NAT_1:2; then len p = 0 by A6, Def3; hence p = <%(0. R)%> by Th14; ::_thesis: verum end; end;