let f be Function of (BOOLEAN *),NAT; :: thesis: ( ( for x being Element of BOOLEAN * holds f . x = ExAbsval x ) implies f is onto )
assume AS1: for x being Element of BOOLEAN * holds f . x = ExAbsval x ; :: thesis: f is onto
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: ( y in NAT implies ex x being object st
( x in BOOLEAN * & y = f . x ) )
assume y in NAT ; :: thesis: ex x being object st
( x in BOOLEAN * & y = f . x )
then reconsider k = y as Nat ;

per cases ( k = 0 or k <> 0 ) ;

suppose C1: k = 0 ; :: thesis: ex x being object st
( x in BOOLEAN * & y = f . x )

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: verum

end;

suppose k <> 0 ; :: thesis: ex x being object st
( x in BOOLEAN * & y = f . x )

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: verum

end;

end;

end;

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