:: Construction of Finite Sequences over Ring and Left-, Right-, and Bi-Modules over a Ring
:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba
::
:: Received September 13, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


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 = {} &amp; Segm 1 = {0} &amp; 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) &amp; 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
proofend;
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
proofend;

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 &amp; ( for m being Nat st m is_at_least_length_of p holds
k <= m ) &amp; l is_at_least_length_of p &amp; ( for m being Nat st m is_at_least_length_of p holds
l <= m ) holds
k = l
proofend;

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 &amp; ( 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 &amp; ( for m being Nat st m is_at_least_length_of p holds
b1 <= m ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st b1 is_at_least_length_of p &amp; ( for m being Nat st m is_at_least_length_of p holds
b1 <= m ) &amp; b2 is_at_least_length_of p &amp; ( 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 &amp; ( 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
proofend;

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

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

::
:: SUPPORT
::
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() &amp; ( for k being Nat st k < F2() holds
p . k = F3(k) ) )
proofend;

theorem Th12: :: ALGSEQ_1:12
for R being non empty ZeroStr
for p, q being AlgSequence of R st len p = len q &amp; ( for k being Nat st k < len p holds
p . k = q . k ) holds
p = q
proofend;

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

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 &amp; it . 0 = x );
existence
 ex b1 being AlgSequence of R st
( len b1 <= 1 &amp; b1 . 0 = x )
proofend;
uniqueness
 for b1, b2 being AlgSequence of R st len b1 <= 1 &amp; b1 . 0 = x &amp; len b2 <= 1 &amp; b2 . 0 = x holds
b1 = b2
proofend;
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 &amp; b3 . 0 = x ) );

Lm3:  for R being non empty ZeroStr
for p being AlgSequence of R st p = <%(0. R)%> holds
len p = 0
proofend;

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 )
proofend;

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

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)} )
proofend;