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 ]

end;

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

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;
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:

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;

end;