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 :: thesis: for u being object st u in dom ((0. L) * p) holds
((0. L) * p) . u = (0_ (n,L)) . u

let u be object ; :: 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 ;
((0. L) * p) . u9 = (0. L) * (p . u9) by POLYNOM7:def 9
.= 0. L by BINOM:1 ;
hence ((0. L) * p) . u = (0_ (n,L)) . u by POLYNOM1:22; :: 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:2; :: thesis: verum