defpred S₁[ Element of NAT , object ] means $2 = 1 --> $1;
A1: for x being Element of NAT ex y being Element of Bags 1 st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of Bags 1 st S₁[x,y]
reconsider y = 1 --> x as object ;
take y ; :: thesis: ( y is set & y is Element of Bags 1 & y is Element of Bags 1 & S₁[x,y] )
thus ( y is set & y is Element of Bags 1 & y is Element of Bags 1 & S₁[x,y] ) by PRE_POLY:def 12; :: thesis: verum

end;

consider f being Function of NAT,(Bags 1) such that
A2: for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for m being Element of NAT holds f . m = 1 --> m
thus for m being Element of NAT holds f . m = 1 --> m by A2; :: thesis: verum