let L be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; :: thesis: for p being sequence of L holds (0. L) * p = 0_. L
let p be sequence of L; :: thesis: (0. L) * p = 0_. L
set t = (0. L) * p;

now :: thesis: for x being object st x in NAT holds
((0. L) * p) . x = (0_. L) . x

let x be object ; :: thesis: ( x in NAT implies ((0. L) * p) . x = (0_. L) . x )
assume x in NAT ; :: thesis: ((0. L) * p) . x = (0_. L) . x
then reconsider i = x as Element of NAT ;
thus ((0. L) * p) . x = (0. L) * (p . i) by POLYNOM5:def 4
.= (0_. L) . x by FUNCOP_1:7 ; :: thesis: verum

end;

hence (0. L) * p = 0_. L by FUNCT_2:12; :: thesis: verum