defpred S₁[ Element of Bags n, Element of L] means ex b being bag of n st
( b = $1 & ex s being FinSequence of the carrier of L st
( $2 = 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) ) ) ) );

A1: now :: thesis: for bb being Element of Bags n ex y being Element of L st S₁[bb,y]

let bb be Element of Bags n; :: thesis: ex y being Element of L st S₁[bb,y]
reconsider b = bb as bag of n ;
defpred S₂[ Nat, set ] means ex b1, b2 being bag of n st
( (decomp b) /. $1 = <*b1,b2*> & $2 = (p . b1) * (q . b2) );

A2: now :: thesis: for k being Nat st k in Seg (len (decomp b)) holds
ex x being Element of L st S₂[k,x]

let k be Nat; :: thesis: ( k in Seg (len (decomp b)) implies ex x being Element of L st S₂[k,x] )
assume k in Seg (len (decomp b)) ; :: thesis: ex x being Element of L st S₂[k,x]
then k in dom (decomp b) by FINSEQ_1:def 3;
then consider b1, b2 being bag of n such that
A3: (decomp b) /. k = <*b1,b2*> and
b = b1 + b2 by PRE_POLY:68;
reconsider x = (p . b1) * (q . b2) as Element of L ;
take x = x; :: thesis: S₂[k,x]
thus S₂[k,x] by A3; :: thesis: verum

end;

consider s being FinSequence of the carrier of L such that
A4: len s = len (decomp b) and
A5: for k being Nat st k in Seg (len (decomp b)) holds
S₂[k,s /. k] from FINSEQ_4:sch 1(A2);
reconsider y = Sum s as Element of L ;
take y = y; :: thesis: S₁[bb,y]
thus S₁[bb,y] :: thesis: verum

proof

take b ; :: thesis: ( b = bb & ex s being FinSequence of the carrier of L st
( y = 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) ) ) ) )
thus b = bb ; :: thesis: ex s being FinSequence of the carrier of L st
( y = 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) ) ) )
take s ; :: thesis: ( y = 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) ) ) )
thus y = Sum s ; :: thesis: ( 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) ) ) )
thus len s = len (decomp b) by A4; :: thesis: 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) )
let k be Element of NAT ; :: thesis: ( k in dom s implies ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) )
assume k in dom s ; :: thesis: ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) )
then k in Seg (len (decomp b)) by A4, FINSEQ_1:def 3;
hence ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by A5; :: thesis: verum

end;

end;

consider P being Function of (Bags n), the carrier of L such that
A6: for b being Element of Bags n holds S₁[b,P . b] from FUNCT_2:sch 3(A1);
reconsider P = P as Function of (Bags n),L ;
reconsider P = P as Series of n,L ;
take P ; :: thesis: for b being bag of n ex s being FinSequence of the carrier of L st
( P . 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) ) ) )
let b be bag of n; :: thesis: ex s being FinSequence of the carrier of L st
( P . 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) ) ) )
reconsider bb = b as Element of Bags n by PRE_POLY:def 12;
S₁[bb,P . bb] by A6;
hence ex s being FinSequence of the carrier of L st
( P . 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: verum