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 )

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

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

end;now :: thesis: for i being Nat st i >= 0 holds

(monomial (a,n)) . i = 0. L

then
0 is_at_least_length_of monomial (a,n)
by ALGSEQ_1:def 2;(monomial (a,n)) . i = 0. L

let i be Nat; :: thesis: ( i >= 0 implies (monomial (a,n)) . b_{1} = 0. L )

assume i >= 0 ; :: thesis: (monomial (a,n)) . b_{1} = 0. L

end;assume i >= 0 ; :: thesis: (monomial (a,n)) . b

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

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

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: verumnow :: thesis: for i being Nat st i >= n + 1 holds

(monomial (a,n)) . i = 0. L

then
n + 1 is_at_least_length_of monomial (a,n)
by ALGSEQ_1:def 2;(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;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

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