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

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

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