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

proof

let y be object ; :: thesis: ( y in NAT implies ex A being object st
( A in Class EqBL2Nat & y = QuBL2Nat . A ) )
assume A0: y in NAT ; :: thesis: ex A being object st
( A in Class EqBL2Nat & y = QuBL2Nat . A )
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: verum

end;

then rng QuBL2Nat = NAT by FUNCT_2:10;
hence QuBL2Nat is onto by FUNCT_2:def 3; :: thesis: verum