let n be Ordinal; :: thesis: for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds p * a = p *' (a | (n,L))

let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for p being Series of n,L
for a being Element of L holds p * a = p *' (a | (n,L))

let p be Series of n,L; :: thesis: for a being Element of L holds p * a = p *' (a | (n,L))
let a be Element of L; :: thesis: p * a = p *' (a | (n,L))
for x being object st x in Bags n holds
(p * a) . x = (p *' (a | (n,L))) . x
proof
set O = a | (n,L);
set cL = the carrier of L;
let x be object ; :: thesis: ( x in Bags n implies (p * a) . x = (p *' (a | (n,L))) . x )
assume x in Bags n ; :: thesis: (p * a) . x = (p *' (a | (n,L))) . x
then reconsider b = x as bag of n ;
A1: for b being Element of Bags n holds (p *' (a | (n,L))) . b = (p . b) * a
proof
let b be Element of Bags n; :: thesis: (p *' (a | (n,L))) . b = (p . b) * a
consider s being FinSequence of the carrier of L such that
A2: (p *' (a | (n,L))) . b = Sum s and
A3: len s = len () and
A4: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( () /. k = <*b1,b2*> & s /. k = (p . b1) * ((a | (n,L)) . b2) ) by POLYNOM1:def 10;
consider t being FinSequence of the carrier of L, s1 being Element of the carrier of L such that
A5: s = t ^ <*s1*> by ;
A6: now :: thesis: Sum t = 0. L
per cases ( t = <*> the carrier of L or t <> <*> the carrier of L ) ;
suppose A7: t <> <*> the carrier of L ; :: thesis: Sum t = 0. L
now :: thesis: for k being Nat st k in dom t holds
t /. k = 0. L
let k be Nat; :: thesis: ( k in dom t implies t /. b1 = 0. L )
A8: len s = (len t) + (len <*s1*>) by
.= (len t) + 1 by FINSEQ_1:39 ;
assume A9: k in dom t ; :: thesis: t /. b1 = 0. L
then A10: t /. k = t . k by PARTFUN1:def 6
.= s . k by ;
k <= len t by ;
then A11: k < len s by ;
A12: 1 <= k by ;
then A13: k in dom () by ;
A14: dom s = dom () by ;
then A15: s /. k = s . k by ;
per cases ( 1 < k or k = 1 ) by ;
suppose A16: 1 < k ; :: thesis: t /. b1 = 0. L
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
consider b1, b2 being bag of n such that
A17: (decomp b) /. k1 = <*b1,b2*> and
A18: s /. k1 = (p . b1) * ((a | (n,L)) . b2) by A4, A14, A13;
b2 <> EmptyBag n by ;
hence t /. k = (p . b1) * (0. L) by
.= 0. L ;
:: thesis: verum
end;
suppose A19: k = 1 ; :: thesis: t /. b1 = 0. L
A20: now :: thesis: not b = EmptyBag n
assume b = EmptyBag n ; :: thesis: contradiction
then decomp b = <*<*(),()*>*> by PRE_POLY:73;
then (len t) + 1 = 0 + 1 by ;
hence contradiction by A7; :: thesis: verum
end;
consider b1, b2 being bag of n such that
A21: (decomp b) /. k = <*b1,b2*> and
A22: s /. k = (p . b1) * ((a | (n,L)) . b2) by A4, A14, A13;
(decomp b) /. 1 = <*(),b*> by PRE_POLY:71;
then ( b1 = EmptyBag n & b2 = b ) by ;
then s . k = (p . ()) * (0. L) by
.= 0. L ;
hence t /. k = 0. L by A10; :: thesis: verum
end;
end;
end;
hence Sum t = 0. L by MATRLIN:11; :: thesis: verum
end;
end;
end;
A23: s . (len s) = (t ^ <*s1*>) . ((len t) + 1) by
.= s1 by FINSEQ_1:42 ;
A24: Sum s = (Sum t) + (Sum <*s1*>) by ;
not s is empty by A3;
then A25: len s in dom s by FINSEQ_5:6;
then consider b1, b2 being bag of n such that
A26: (decomp b) /. (len s) = <*b1,b2*> and
A27: s /. (len s) = (p . b1) * ((a | (n,L)) . b2) by A4;
A28: s /. (len s) = s . (len s) by ;
(decomp b) /. (len s) = <*b,()*> by ;
then A29: ( b1 = b & b2 = EmptyBag n ) by ;
Sum <*s1*> = s1 by RLVECT_1:44
.= (p . b) * a by A27, A29, A28, A23, Th18 ;
hence (p *' (a | (n,L))) . b = (p . b) * a by ; :: thesis: verum
end;
b is Element of Bags n by PRE_POLY:def 12;
then (p *' (a | (n,L))) . b = (p . b) * a by A1
.= (p * a) . b by Def10 ;
hence (p * a) . x = (p *' (a | (n,L))) . x ; :: thesis: verum
end;
hence p * a = p *' (a | (n,L)) ; :: thesis: verum