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 object 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 H_{1}( 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 = H_{1}(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 Th2;

hence ex p being AlgSequence of R st len p = k by A3, XXREAL_0:1; :: thesis: verum

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

consider p being AlgSequence of R such that

A3: ( len p <= k & ( for i being Nat st i < k holds

p . i = H

for i being Nat st i < k holds

p . i <> 0. R by A2, A3;

then len p >= k by Th2;

hence ex p being AlgSequence of R st len p = k by A3, XXREAL_0:1; :: thesis: verum