let it1, it2 be Series of n,L; :: thesis: ( ( for b being bag of n ex s being FinSequence of the carrier of L st
( it1 . b = Sum s & len s = len (decomp b) & ( 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) * (q . b2) ) ) ) ) & ( for b being bag of n ex s being FinSequence of the carrier of L st
( it2 . b = Sum s & len s = len (decomp b) & ( 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) * (q . b2) ) ) ) ) implies it1 = it2 )
assume that
A7: for b being bag of n ex s being FinSequence of the carrier of L st
( it1 . b = Sum s & len s = len (decomp b) & ( 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) * (q . b2) ) ) ) and
A8: for b being bag of n ex s being FinSequence of the carrier of L st
( it2 . b = Sum s & len s = len (decomp b) & ( 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) * (q . b2) ) ) ) ; :: thesis: it1 = it2
reconsider ita = it1, itb = it2 as Function of (Bags n), the carrier of L ;
now :: thesis: for b being Element of Bags n holds ita . b = itb . b
let b be Element of Bags n; :: thesis: ita . b = itb . b
consider sa being FinSequence of the carrier of L such that
A9: ita . b = Sum sa and
A10: len sa = len (decomp b) and
A11: for k being Element of NAT st k in dom sa holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & sa /. k = (p . b1) * (q . b2) ) by A7;
consider sb being FinSequence of the carrier of L such that
A12: itb . b = Sum sb and
A13: len sb = len (decomp b) and
A14: for k being Element of NAT st k in dom sb holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & sb /. k = (p . b1) * (q . b2) ) by A8;
now :: thesis: for k being Nat st 1 <= k & k <= len sa holds
sa . k = sb . k
let k be Nat; :: thesis: ( 1 <= k & k <= len sa implies sa . k = sb . k )
assume A15: ( 1 <= k & k <= len sa ) ; :: thesis: sa . k = sb . k
then A16: k in dom sa by FINSEQ_3:25;
then A17: sa /. k = sa . k by PARTFUN1:def 6;
A18: k in dom sb by A10, A13, A15, FINSEQ_3:25;
then A19: sb /. k = sb . k by PARTFUN1:def 6;
consider ab1, ab2 being bag of n such that
A20: (decomp b) /. k = <*ab1,ab2*> and
A21: sa /. k = (p . ab1) * (q . ab2) by A11, A16;
consider bb1, bb2 being bag of n such that
A22: (decomp b) /. k = <*bb1,bb2*> and
A23: sb /. k = (p . bb1) * (q . bb2) by A14, A18;
ab1 = bb1 by A20, A22, FINSEQ_1:77;
hence sa . k = sb . k by A20, A21, A22, A23, A17, A19, FINSEQ_1:77; :: thesis: verum
end;
hence ita . b = itb . b by A9, A10, A12, A13, FINSEQ_1:14; :: thesis: verum
end;
hence it1 = it2 ; :: thesis: verum