let n be Ordinal; :: thesis: for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds p *' (0_ n,L) = 0_ n,L
let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Series of n,L holds p *' (0_ n,L) = 0_ n,L
let p be Series of n,L; :: thesis: p *' (0_ n,L) = 0_ n,L
set Z = 0_ n,L;

now

let b be Element of Bags n; :: thesis: (p *' (0_ n,L)) . b = (0_ n,L) . b
consider s being FinSequence of the carrier of L such that
A1: (p *' (0_ n,L)) . b = Sum s and
len s = len (decomp b) and
A2: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((0_ n,L) . b2) ) by Def26;

now

let k be Nat; :: thesis: ( k in dom s implies s /. k = 0. L )
assume k in dom s ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
(decomp b) /. k = <*b1,b2*> and
A3: s /. k = (p . b1) * ((0_ n,L) . b2) by A2;
thus s /. k = (p . b1) * (0. L) by A3, Th81
.= 0. L by VECTSP_1:36 ; :: thesis: verum

end;

then Sum s = 0. L by MATRLIN:15;
hence (p *' (0_ n,L)) . b = (0_ n,L) . b by A1, Th81; :: thesis: verum

end;

hence p *' (0_ n,L) = 0_ n,L by FUNCT_2:113; :: thesis: verum