let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for p being Polynomial of L holds len ((0. L) * p) = 0
let p be Polynomial of L; :: thesis: len ((0. L) * p) = 0
0 is_at_least_length_of (0. L) * p

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not 0 <= i or ((0. L) * p) . i = 0. L )
assume i >= 0 ; :: thesis: ((0. L) * p) . i = 0. L
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
thus ((0. L) * p) . i = (0. L) * (p . ii) by Def4
.= 0. L ; :: thesis: verum

end;

hence len ((0. L) * p) = 0 by ALGSEQ_1:def 3; :: thesis: verum