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

proof

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

now :: thesis: not m < n + 1

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

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

end;

A3: n + 1 in NAT by ORDINAL1:def 12;
for i being Nat st i >= n + 1 holds
(unital_poly (L,n)) . i = 0. L

proof

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

now :: thesis: not i = n

A5: n + 0 < n + 1 by XREAL_1:8;
assume i = n ; :: thesis: contradiction
hence contradiction by A4, A5; :: thesis: verum

end;

hence (unital_poly (L,n)) . i = 0. L by A4, Th39; :: thesis: verum

end;

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