:: 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;