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 )
assume k >= 1 ; :: thesis: deg (qpoly k,z) = k - 1
then k - 1 >= 1 - 1 by XREAL_1:11;
then reconsider k' = k - 1 as Element of NAT by INT_1:16;
set p = qpoly k,z;
for i being Nat st i >= k holds
(qpoly k,z) . i = 0. L by Def4;
then A1: k is_at_least_length_of qpoly k,z by ALGSEQ_1:def 3;
A2: (k - k') - 1 = 0 ;
k - 1 < k - 0 by XREAL_1:12;
then (qpoly k,z) . (k - 1) = (power L) . z,0 by A2, Def4
.= 1_ L by GROUP_1:def 8 ;
then A3: (qpoly k,z) . (k - 1) <> 0. L ;

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 k' + 1 > m ;
then k' >= m by NAT_1:13;
hence contradiction by A3, A4, ALGSEQ_1:def 3; :: thesis: verum

end;

hence k <= m ; :: thesis: verum

end;

hence deg (qpoly k,z) = k - 1 by A1, ALGSEQ_1:def 4; :: thesis: verum