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

now

assume A2: i = n ; :: thesis: contradiction
n + 0 < n + 1 by XREAL_1:10;
hence contradiction by A1, A2; :: thesis: verum

end;

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

end;

then A3: n + 1 is_at_least_length_of unital_poly L,n by ALGSEQ_1:def 3;
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 A4: 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 & (unital_poly L,n) . n = 1_ L ) by A4, Th42, ALGSEQ_1:def 3;
hence contradiction ; :: thesis: verum

end;

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

end;

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