let R be non degenerated unital doubleLoopStr ; :: thesis: for n being non trivial Nat holds deg (X^ (n,R)) = n
let n be non trivial Nat; :: thesis: deg (X^ (n,R)) = n
set q = X^ (n,R);
A1: n >= 2 by NAT_2:29;

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

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

end;

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

let m be Nat; :: thesis: ( m is_at_least_length_of X^ (n,R) implies n + 1 <= m )
assume X: m is_at_least_length_of X^ (n,R) ; :: thesis: n + 1 <= m

now :: thesis: not n + 1 > m

assume Y: n + 1 > m ; :: thesis: contradiction
(X^ (n,R)) . 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,R)) = n + 1 by A9, ALGSEQ_1:def 3, ALGSEQ_1:def 2;
then deg (X^ (n,R)) = (n + 1) - 1 by HURWITZ:def 2;
hence deg (X^ (n,R)) = n ; :: thesis: verum