begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
:: deftheorem ALGSEQ_1:def 1 :
canceled;
:: deftheorem Def2 defines finite-Support ALGSEQ_1:def 2 :
:: deftheorem Def3 defines is_at_least_length_of ALGSEQ_1:def 3 :
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
Lm2:
for R being non empty ZeroStr
for p being AlgSequence of R ex k being Element of NAT st
( k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds
k <= n ) )
Lm3:
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
:: deftheorem Def4 defines len ALGSEQ_1:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th22:
theorem
canceled;
theorem Th24:
theorem Th25:
:: deftheorem defines support ALGSEQ_1:def 5 :
theorem
canceled;
theorem
theorem Th28:
theorem
:: deftheorem Def6 defines <% ALGSEQ_1:def 6 :
Lm4:
for R being non empty ZeroStr
for p being AlgSequence of R st p = <%(0. R)%> holds
len p = 0
theorem
canceled;
theorem Th31:
theorem
theorem Th33:
theorem