let f be Function of (BOOLEAN *),NAT; :: thesis:
assume AS1: for x being Element of BOOLEAN * holds f . x = ExAbsval x ; :: thesis:
for y being object st y in NAT holds
ex x being object st
( x in BOOLEAN * & y = f . x )

proof

let y be object ; :: thesis:
assume y in NAT ; :: thesis:
then reconsider k = y as Nat ;

per cases ;

suppose C1: k = 0 ; :: thesis:

reconsider x = <*> BOOLEAN as Element of BOOLEAN * by FINSEQ_1:def 11;
len x = 0 ;
then ExAbsval x = 0 by D100;
then y = f . x by AS1, C1;
hence ex x being object st
( x in BOOLEAN * & y = f . x ) ; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then consider n being Nat such that
A1: ( 2 to_power n <= k & k < 2 to_power (n + 1) ) by LM001;
set xn = (n + 1) -BinarySequence k;
reconsider x = (n + 1) -BinarySequence k as Element of BOOLEAN * by FINSEQ_1:def 11;
ExAbsval x = Absval ((n + 1) -BinarySequence k) by Def100
.= k by A1, BINARI_3:35 ;
then y = f . x by AS1;
hence ex x being object st
( x in BOOLEAN * & y = f . x ) ; :: thesis:

end;

end;

end;

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