let n be set ; :: thesis: for L being non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr
for p being Series of n,L holds (0. L) * p = 0_ n,L
let L be non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr ; :: thesis: for p being Series of n,L holds (0. L) * p = 0_ n,L
let p be Series of n,L; :: thesis: (0. L) * p = 0_ n,L
set op = (0. L) * p;

A1: now

let u be set ; :: thesis: ( u in dom ((0. L) * p) implies ((0. L) * p) . u = (0_ n,L) . u )
assume u in dom ((0. L) * p) ; :: thesis: ((0. L) * p) . u = (0_ n,L) . u
then reconsider u9 = u as bag of n by PRE_POLY:def 12;
((0. L) * p) . u9 = (0. L) * (p . u9) by POLYNOM7:def 10
.= 0. L by BINOM:1 ;
hence ((0. L) * p) . u = (0_ n,L) . u by POLYNOM1:81; :: thesis: verum

end;

dom ((0. L) * p) = Bags n by FUNCT_2:def 1
.= dom (0_ n,L) by FUNCT_2:def 1 ;
hence (0. L) * p = 0_ n,L by A1, FUNCT_1:9; :: thesis: verum