defpred S₁[ set , object ] means ex x being object st
( x in $1 & $2 = BL2Nat . x );
A1: for A being Element of Class EqBL2Nat ex y being Element of NAT st S₁[A,y]

proof

let A be Element of Class EqBL2Nat; :: thesis: ex y being Element of NAT st S₁[A,y]
A is Subset of (BOOLEAN *) by TARSKI:def 3;
then consider x being object such that
A2: ( x in BOOLEAN * & A = Class (EqBL2Nat,x) ) by EQREL_1:def 3;
reconsider y = x as Element of BOOLEAN * by A2;
set z = BL2Nat . y;
take BL2Nat . y ; :: thesis: S₁[A,BL2Nat . y]
thus S₁[A,BL2Nat . y] by A2, EQREL_1:20; :: thesis: verum

end;

consider f being Function of (Class EqBL2Nat),NAT such that
A2: for A being Element of Class EqBL2Nat holds S₁[A,f . A] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for A being Element of Class EqBL2Nat ex x being object st
( x in A & f . A = BL2Nat . x )
thus for A being Element of Class EqBL2Nat ex x being object st
( x in A & f . A = BL2Nat . x ) by A2; :: thesis: verum