for y being object st y in NAT holds
ex A being object st
( A in Class EqBL2Nat & y = QuBL2Nat . A )

let y be object ; :: thesis:
assume A0: y in NAT ; :: thesis:
then reconsider k = y as Nat ;
rng BL2Nat = NAT by FUNCT_2:def 3;
then consider x being object such that
A1: ( x in BOOLEAN * & y = BL2Nat . x ) by FUNCT_2:11, A0;
reconsider A = Class (EqBL2Nat,x) as Element of Class EqBL2Nat by EQREL_1:def 3, A1;
consider x1 being object such that
A2: ( x1 in A & QuBL2Nat . A = BL2Nat . x1 ) by Def400;
[x1,x] in EqBL2Nat by A2, EQREL_1:19;
then BL2Nat . x1 = BL2Nat . x by Def300;
hence ex A being object st
( A in Class EqBL2Nat & y = QuBL2Nat . A ) by A1, A2; :: thesis:

end;