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 :: thesis: for b being Element of Bags n holds (p *' (0_ (n,L))) . b = (0_ (n,L)) . b

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 Def10;

now :: thesis: for k being Nat st k in dom s holds
s /. k = 0. L

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, Th22
.= 0. L ; :: thesis: verum

end;

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

end;

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