let L be non empty non degenerated well-unital doubleLoopStr ; :: thesis: for z being Element of L
for k being Element of NAT st k >= 1 holds
deg (qpoly k,z) = k - 1
let z be Element of L; :: thesis: for k being Element of NAT st k >= 1 holds
deg (qpoly k,z) = k - 1
let k be Element of NAT ; :: thesis: ( k >= 1 implies deg (qpoly k,z) = k - 1 )
set p = qpoly k,z;
A1: k - 1 < k - 0 by XREAL_1:12;
assume k >= 1 ; :: thesis: deg (qpoly k,z) = k - 1
then k - 1 >= 1 - 1 by XREAL_1:11;
then reconsider k9 = k - 1 as Element of NAT by INT_1:16;
(k - k9) - 1 = 0 ;
then (qpoly k,z) . (k - 1) = (power L) . z,0 by A1, Def4
.= 1_ L by GROUP_1:def 8 ;
then A2: (qpoly k,z) . (k - 1) <> 0. L ;

A3: now

let m be Nat; :: thesis: ( m is_at_least_length_of qpoly k,z implies k <= m )
assume A4: m is_at_least_length_of qpoly k,z ; :: thesis: k <= m

now

assume k > m ; :: thesis: contradiction
then k9 + 1 > m ;
then k9 >= m by NAT_1:13;
hence contradiction by A2, A4, ALGSEQ_1:def 3; :: thesis: verum

end;

hence k <= m ; :: thesis: verum

end;

for i being Nat st i >= k holds
(qpoly k,z) . i = 0. L by Def4;
then k is_at_least_length_of qpoly k,z by ALGSEQ_1:def 3;
hence deg (qpoly k,z) = k - 1 by A3, ALGSEQ_1:def 4; :: thesis: verum