let L be non empty non degenerated well-unital doubleLoopStr ; :: thesis: for n being non empty Element of NAT holds len (unital_poly (L,n)) = n + 1
let n be non empty 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

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 Th42; :: thesis: verum

end;

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

end;

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 A3: i >= n + 1 ; :: thesis: (unital_poly (L,n)) . i = 0. L

now

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

end;

hence (unital_poly (L,n)) . i = 0. L by A3, Th43; :: 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; :: thesis: verum