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 :: thesis: for b being Element of Bags n holds ((0_ (n,L)) *' p) . b = (0_ (n,L)) . b
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 n st
( (decomp b) /. k = <*b1,b2*> & s /. k = ((0_ (n,L)) . b1) * (p . b2) ) by POLYNOM1:def 10;
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 = ((0_ (n,L)) . b1) * (p . b2) by A2;
thus s /. k = (0. L) * (p . b2) by A3, POLYNOM1:22
.= 0. L ; :: thesis: verum
end;
then Sum s = 0. L by MATRLIN:11;
hence ((0_ (n,L)) *' p) . b = (0_ (n,L)) . b by A1, POLYNOM1:22; :: thesis: verum
end;
hence (0_ (n,L)) *' p = 0_ (n,L) by FUNCT_2:63; :: thesis: verum