let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for n being Element of NAT
for a being Element of L holds
( ( a <> 0. L implies len (monomial (a,n)) = n + 1 ) & ( a = 0. L implies len (monomial (a,n)) = 0 ) & len (monomial (a,n)) <= n + 1 )
let n be Element of NAT ; :: thesis: for a being Element of L holds
( ( a <> 0. L implies len (monomial (a,n)) = n + 1 ) & ( a = 0. L implies len (monomial (a,n)) = 0 ) & len (monomial (a,n)) <= n + 1 )
let a be Element of L; :: thesis: ( ( a <> 0. L implies len (monomial (a,n)) = n + 1 ) & ( a = 0. L implies len (monomial (a,n)) = 0 ) & len (monomial (a,n)) <= n + 1 )

A1: now :: thesis: ( a = 0. L implies len (monomial (a,n)) = 0 )

assume A2: a = 0. L ; :: thesis: len (monomial (a,n)) = 0

now :: thesis: for i being Nat st i >= 0 holds
(monomial (a,n)) . i = 0. L

let i be Nat; :: thesis: ( i >= 0 implies (monomial (a,n)) . b₁ = 0. L )
assume i >= 0 ; :: thesis: (monomial (a,n)) . b₁ = 0. L

per cases ( i = n or i <> n ) ;

suppose i = n ; :: thesis: (monomial (a,n)) . b₁ = 0. L

thus (monomial (a,n)) . i = 0. L by A2, Def5; :: thesis: verum

end;

suppose i <> n ; :: thesis: (monomial (a,n)) . b₁ = 0. L

hence (monomial (a,n)) . i = 0. L by Def5; :: thesis: verum

end;

end;

end;

then 0 is_at_least_length_of monomial (a,n) by ALGSEQ_1:def 2;
hence len (monomial (a,n)) = 0 by ALGSEQ_1:def 3; :: thesis: verum

end;

now :: thesis: ( a <> 0. L implies len (monomial (a,n)) = n + 1 )

now :: thesis: for i being Nat st i >= n + 1 holds
(monomial (a,n)) . i = 0. L

let i be Nat; :: thesis: ( i >= n + 1 implies (monomial (a,n)) . i = 0. L )
assume i >= n + 1 ; :: thesis: (monomial (a,n)) . i = 0. L
then i > n by NAT_1:13;
hence (monomial (a,n)) . i = 0. L by Def5; :: thesis: verum

end;

then n + 1 is_at_least_length_of monomial (a,n) by ALGSEQ_1:def 2;
then A3: len (monomial (a,n)) <= n + 1 by ALGSEQ_1:def 3;
assume a <> 0. L ; :: thesis: len (monomial (a,n)) = n + 1
then (monomial (a,n)) . n <> 0. L by Def5;
then len (monomial (a,n)) > n by ALGSEQ_1:8;
then len (monomial (a,n)) >= n + 1 by NAT_1:13;
hence len (monomial (a,n)) = n + 1 by A3, XXREAL_0:1; :: thesis: verum

end;

hence ( ( a <> 0. L implies len (monomial (a,n)) = n + 1 ) & ( a = 0. L implies len (monomial (a,n)) = 0 ) & len (monomial (a,n)) <= n + 1 ) by A1; :: thesis: verum