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);

then deg (npoly (R,n)) = (n + 1) - 1 by HURWITZ:def 2;

hence deg (npoly (R,n)) = n ; :: thesis: verum

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

(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;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

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

n + 1 <= m

then
len (npoly (R,n)) = n + 1
by A9, ALGSEQ_1:def 3, ALGSEQ_1:def 2;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

end;assume X: m is_at_least_length_of npoly (R,n) ; :: thesis: n + 1 <= m

now :: thesis: not n + 1 > m

hence
n + 1 <= m
; :: thesis: verumassume 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;(npoly (R,n)) . n = 1. R by Lm10;

hence contradiction by X, Y, NAT_1:13; :: thesis: verum

then deg (npoly (R,n)) = (n + 1) - 1 by HURWITZ:def 2;

hence deg (npoly (R,n)) = n ; :: thesis: verum