defpred S₁[ object ] means $1 is bag of X;
consider A being set such that
A1: for x being object holds
( x in A iff ( x in Funcs (X,NAT) & S₁[x] ) ) from XBOOLE_0:sch 1();
take A ; :: thesis: for x being set holds
( x in A iff x is bag of X )
let x be set ; :: thesis: ( x in A iff x is bag of X )
thus ( x in A implies x is bag of X ) by A1; :: thesis: ( x is bag of X implies x in A )
assume A2: x is bag of X ; :: thesis: x in A
then reconsider b = x as bag of X ;
( dom b = X & rng b c= NAT ) by PARTFUN1:def 2, VALUED_0:def 6;
then x in Funcs (X,NAT) by FUNCT_2:def 2;
hence x in A by A1, A2; :: thesis: verum