:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba

::

:: Received September 13, 1990

:: Copyright (c) 1990-2017 Association of Mizar Users

definition

let R be non empty ZeroStr ;

let F be sequence of R;

( F is finite-Support iff ex n being Nat st

for i being Nat st i >= n holds

F . i = 0. R )

end;
let F be sequence of R;

redefine attr F 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;

compatibility ex n being Nat st

for i being Nat st i >= n holds

F . i = 0. R;

( F is finite-Support iff ex n being Nat st

for i being Nat st i >= n holds

F . i = 0. R )

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

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 ;

ex b_{1} being sequence of R st b_{1} is finite-Support

end;
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 b

proof end;

definition

let R be non empty ZeroStr ;

let p be AlgSequence of R;

let k be Nat;

end;
let p be AlgSequence of R;

let k be Nat;

pred k is_at_least_length_of p means :Def2: :: ALGSEQ_1:def 2

for i being Nat st i >= k holds

p . i = 0. R;

for i being Nat st i >= k holds

p . i = 0. R;

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

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

definition

let R be non empty ZeroStr ;

let p be AlgSequence of R;

ex b_{1} being Element of NAT st

( b_{1} is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds

b_{1} <= m ) )

for b_{1}, b_{2} being Element of NAT st b_{1} is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds

b_{1} <= m ) & b_{2} is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds

b_{2} <= m ) holds

b_{1} = b_{2}

end;
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 ( it is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds

it <= m ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines len ALGSEQ_1:def 3 :

for R being non empty ZeroStr

for p being AlgSequence of R

for b_{3} being Element of NAT holds

( b_{3} = len p iff ( b_{3} is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds

b_{3} <= m ) ) );

for R being non empty ZeroStr

for p being AlgSequence of R

for b

( b

b

::$CT 7

theorem Th1: :: 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

for R being non empty ZeroStr

for p being AlgSequence of R st i >= len p holds

p . i = 0. R

proof end;

theorem Th2: :: 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

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

theorem Th3: :: 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

for R being non empty ZeroStr

for p being AlgSequence of R st len p = k + 1 holds

p . k <> 0. R

proof end;

::$CT

theorem Th4: :: 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

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

for k being Nat ex p being AlgSequence of R st len p = k

proof end;

definition

let R be non empty ZeroStr ;

let x be Element of R;

existence

ex b_{1} being AlgSequence of R st

( len b_{1} <= 1 & b_{1} . 0 = x )

for b_{1}, b_{2} being AlgSequence of R st len b_{1} <= 1 & b_{1} . 0 = x & len b_{2} <= 1 & b_{2} . 0 = x holds

b_{1} = b_{2}

end;
let x be Element of R;

existence

ex b

( len b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines <% ALGSEQ_1:def 5 :

for R being non empty ZeroStr

for x being Element of R

for b_{3} being AlgSequence of R holds

( b_{3} = <%x%> iff ( len b_{3} <= 1 & b_{3} . 0 = x ) );

for R being non empty ZeroStr

for x being Element of R

for b

( b

Lm2: for R being non empty ZeroStr

for p being AlgSequence of R st p = <%(0. R)%> holds

len p = 0

proof end;

::$CT

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

for p being AlgSequence of R holds

( p = <%(0. R)%> iff rng p = {(0. R)} )

proof end;