let L be non empty non degenerated well-unital doubleLoopStr ; :: thesis: for n being non zero Element of NAT holds len (unital_poly (L,n)) = n + 1

let n be non zero Element of NAT ; :: thesis: len (unital_poly (L,n)) = n + 1

A1: for m being Nat st m is_at_least_length_of unital_poly (L,n) holds

n + 1 <= m

for i being Nat st i >= n + 1 holds

(unital_poly (L,n)) . i = 0. L

hence len (unital_poly (L,n)) = n + 1 by A1, ALGSEQ_1:def 3, A3; :: thesis: verum

let n be non zero Element of NAT ; :: thesis: len (unital_poly (L,n)) = n + 1

A1: for m being Nat st m is_at_least_length_of unital_poly (L,n) holds

n + 1 <= m

proof

A3:
n + 1 in NAT
by ORDINAL1:def 12;
let m be Nat; :: thesis: ( m is_at_least_length_of unital_poly (L,n) implies n + 1 <= m )

assume A2: m is_at_least_length_of unital_poly (L,n) ; :: thesis: n + 1 <= m

end;assume A2: m is_at_least_length_of unital_poly (L,n) ; :: thesis: n + 1 <= m

now :: thesis: not m < n + 1

hence
n + 1 <= m
; :: thesis: verumassume
m < n + 1
; :: thesis: contradiction

then m <= n by NAT_1:13;

then (unital_poly (L,n)) . n = 0. L by A2, ALGSEQ_1:def 2;

hence contradiction by Th38; :: thesis: verum

end;then m <= n by NAT_1:13;

then (unital_poly (L,n)) . n = 0. L by A2, ALGSEQ_1:def 2;

hence contradiction by Th38; :: thesis: verum

for i being Nat st i >= n + 1 holds

(unital_poly (L,n)) . i = 0. L

proof

then
n + 1 is_at_least_length_of unital_poly (L,n)
by ALGSEQ_1:def 2;
let i be Nat; :: thesis: ( i >= n + 1 implies (unital_poly (L,n)) . i = 0. L )

assume A4: i >= n + 1 ; :: thesis: (unital_poly (L,n)) . i = 0. L

end;assume A4: i >= n + 1 ; :: thesis: (unital_poly (L,n)) . i = 0. L

now :: thesis: not i = n

hence
(unital_poly (L,n)) . i = 0. L
by A4, Th39; :: thesis: verumA5:
n + 0 < n + 1
by XREAL_1:8;

assume i = n ; :: thesis: contradiction

hence contradiction by A4, A5; :: thesis: verum

end;assume i = n ; :: thesis: contradiction

hence contradiction by A4, A5; :: thesis: verum

hence len (unital_poly (L,n)) = n + 1 by A1, ALGSEQ_1:def 3, A3; :: thesis: verum