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

now

let b be Element of Bags n; :: thesis: ((0_ n,L) *' p) . b = (0_ n,L) . b
consider s being FinSequence of L such that
A1: ((0_ n,L) *' p) . 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 st
( (decomp b) /. k = <*b1,b2*> & s /. k = ((0_ n,L) . b1) * (p . b2) ) by POLYNOM1:def 26;

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 such that
(decomp b) /. k = <*b1,b2*> and
A3: s /. k = ((0_ n,L) . b1) * (p . b2) by A2;
thus s /. k = (0. L) * (p . b2) by A3, POLYNOM1:81
.= 0. L by VECTSP_1:39 ; :: thesis: verum

end;

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

end;

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