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