let k be Nat; :: thesis: for R being non empty ZeroStr

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

p . k <> 0. R

let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R st len p = k + 1 holds

p . k <> 0. R

let p be AlgSequence of R; :: thesis: ( len p = k + 1 implies p . k <> 0. R )

assume A1: len p = k + 1 ; :: thesis: p . k <> 0. R

then k < len p by XREAL_1:29;

then not k is_at_least_length_of p by Def3;

then consider i being Nat such that

A2: i >= k and

A3: p . i <> 0. R ;

i < k + 1 by A1, A3, Th1;

then i <= k by NAT_1:13;

hence p . k <> 0. R by A2, A3, XXREAL_0:1; :: thesis: verum

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

p . k <> 0. R

let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R st len p = k + 1 holds

p . k <> 0. R

let p be AlgSequence of R; :: thesis: ( len p = k + 1 implies p . k <> 0. R )

assume A1: len p = k + 1 ; :: thesis: p . k <> 0. R

then k < len p by XREAL_1:29;

then not k is_at_least_length_of p by Def3;

then consider i being Nat such that

A2: i >= k and

A3: p . i <> 0. R ;

i < k + 1 by A1, A3, Th1;

then i <= k by NAT_1:13;

hence p . k <> 0. R by A2, A3, XXREAL_0:1; :: thesis: verum