defpred S₁[ Element of Bags 1, object ] means $2 = $1 . 0;
A1: for x being Element of Bags 1 ex y being Element of NAT st S₁[x,y] ;
consider f being Function of (Bags 1),NAT such that
A2: for x being Element of Bags 1 holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for b being Element of Bags 1 holds f . b = b . 0
thus for b being Element of Bags 1 holds f . b = b . 0 by A2; :: thesis: verum