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
A1: 0 is_at_least_length_of (0. L) * p

proof

let i be Nat; :: according to ALGSEQ_1:def 3 :: 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 13;
thus ((0. L) * p) . i = (0. L) * (p . ii) by Def3
.= 0. L by VECTSP_1:39 ; :: thesis: verum

end;

thus len ((0. L) * p) = 0 by A1, ALGSEQ_1:def 4; :: thesis: verum