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