let I be set ; :: thesis:
defpred S₁[ Nat] means for p being Bags I -valued FinSequence st len p = $1 holds
for i being object st i in support (Sum p) holds
ex b being bag of I st
( b in rng p & i in support b );
A1: S₁[ 0 ]

proof

let p be Bags I -valued FinSequence; :: thesis:
assume A2: len p = 0 ; :: thesis:
let i be object ; :: thesis:
assume Z0: i in support (Sum p) ; :: thesis:
( p = {} & {} = <*> (Bags I) ) by A2;
then i in support (EmptyBag I) by Z0, Th21;
hence ex b being bag of I st
( b in rng p & i in support b ) ; :: thesis:

end;

A3: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis:
assume A4: S₁[j] ; :: thesis:
let p be Bags I -valued FinSequence; :: thesis:
assume A2: len p = j + 1 ; :: thesis:
consider w being FinSequence, x being set such that
A5: ( p = w ^ <*x*> & len w = j ) by A2, TREES_2:3;
reconsider w = w, xx = <*x*> as Bags I -valued FinSequence by A5, Lem8;
len xx = 1 by FINSEQ_1:40;
then 1 in dom xx by FINSEQ_3:25;
then ( x = xx . 1 & xx . 1 in Bags I ) by FUNCT_1:102, FINSEQ_1:40;
then reconsider x = x as Element of Bags I ;
Sum p = (Sum w) + x by A5, Th22;
then A6: support (Sum p) = (support (Sum w)) \/ (support x) by PRE_POLY:38;
let i be object ; :: thesis:
assume i in support (Sum p) ; :: thesis:

per cases by A6, XBOOLE_0:def 3;

suppose i in support (Sum w) ; :: thesis:

then consider b being bag of I such that
A7: ( b in rng w & i in support b ) by A4, A5;
take b ; :: thesis:
rng p = (rng w) \/ (rng xx) by A5, FINSEQ_1:31;
hence ( b in rng p & i in support b ) by A7, XBOOLE_0:def 3; :: thesis:

end;

suppose A8: i in support x ; :: thesis:

take b = x; :: thesis:
( rng p = (rng w) \/ (rng xx) & x in {x} & {x} = rng xx ) by A5, FINSEQ_1:31, FINSEQ_1:39, TARSKI:def 1;
hence ( b in rng p & i in support b ) by A8, XBOOLE_0:def 3; :: thesis:

end;

end;

end;

let p be Bags I -valued FinSequence; :: thesis:
for j being Nat holds S₁[j] from NAT_1:sch 2(A1, A3);
then S₁[ len p] ;
hence for i being object st i in support (Sum p) holds
ex b being bag of I st
( b in rng p & i in support b ) ; :: thesis: