let R be non degenerated unital doubleLoopStr ; :: thesis: for a being Element of R
for n being non zero Nat holds deg (X^ (n,a)) = n
let a be Element of R; :: thesis: for n being non zero Nat holds deg (X^ (n,a)) = n
let n be non zero Nat; :: thesis: deg (X^ (n,a)) = n
set q = X^ (n,a);

A9: now :: thesis: for i being Nat st i >= n + 1 holds
(X^ (n,a)) . i = 0. R

let i be Nat; :: thesis: ( i >= n + 1 implies (X^ (n,a)) . i = 0. R )
assume i >= n + 1 ; :: thesis: (X^ (n,a)) . i = 0. R
then ( i <> n & i <> 0 ) by NAT_1:13;
hence (X^ (n,a)) . i = 0. R by Lm11; :: thesis: verum

end;

now :: thesis: for m being Nat st m is_at_least_length_of X^ (n,a) holds
n + 1 <= m

let m be Nat; :: thesis: ( m is_at_least_length_of X^ (n,a) implies n + 1 <= m )
assume m is_at_least_length_of X^ (n,a) ; :: thesis: n + 1 <= m
then X: for i being Nat st i >= m holds
(X^ (n,a)) . i = 0. R by ALGSEQ_1:def 2;

now :: thesis: not n + 1 > m

assume Y: n + 1 > m ; :: thesis: contradiction
(X^ (n,a)) . n = 1. R by Lm10;
hence contradiction by X, Y, NAT_1:13; :: thesis: verum

end;

hence n + 1 <= m ; :: thesis: verum

end;

then len (X^ (n,a)) = n + 1 by A9, ALGSEQ_1:def 3, ALGSEQ_1:def 2;
then deg (X^ (n,a)) = (n + 1) - 1 by HURWITZ:def 2;
hence deg (X^ (n,a)) = n ; :: thesis: verum