let n be Nat; :: thesis: for R being non degenerated unital doubleLoopStr holds deg (npoly (R,n)) = n
let R be non degenerated unital doubleLoopStr ; :: thesis: deg (npoly (R,n)) = n
set q = npoly (R,n);

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

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

end;

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

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

now :: thesis: not n + 1 > m

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