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:10;
assume k >= 1 ; :: thesis: deg (qpoly (k,z)) = k - 1
then k - 1 >= 1 - 1 by XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
(k - k9) - 1 = 0 ;
then (qpoly (k,z)) . (k - 1) = (power L) . (z,0) by A1, Def4
.= 1_ L by GROUP_1:def 7 ;
then A2: (qpoly (k,z)) . (k - 1) <> 0. L ;

A3: now :: thesis: for m being Nat st m is_at_least_length_of qpoly (k,z) holds
k <= m

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 :: thesis: not k > m

assume k > m ; :: thesis: contradiction
then k9 + 1 > m ;
then k9 >= m by NAT_1:13;
hence contradiction by A2, A4, ALGSEQ_1:def 2; :: 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 2;
hence deg (qpoly (k,z)) = k - 1 by A3, ALGSEQ_1:def 3; :: thesis: verum