let G, H be non empty set ; :: thesis: for h being Function of G,H holds
( h is onto iff for c being Element of H ex a being Element of G st h . a = c )
let h be Function of G,H; :: thesis: ( h is onto iff for c being Element of H ex a being Element of G st h . a = c )

hereby :: thesis: ( ( for c being Element of H ex a being Element of G st h . a = c ) implies h is onto )

assume h is onto ; :: thesis: for c being Element of H ex a being Element of G st h . a = c
then A1: rng h = H ;
let c be Element of H; :: thesis: ex a being Element of G st h . a = c
ex a being object st
( a in G & h . a = c ) by A1, FUNCT_2:11;
hence ex a being Element of G st h . a = c ; :: thesis: verum

end;

assume A2: for c being Element of H ex a being Element of G st h . a = c ; :: thesis: h is onto
for y being object st y in H holds
ex x being object st
( x in G & y = h . x )

proof

let y be object ; :: thesis: ( y in H implies ex x being object st
( x in G & y = h . x ) )
assume y in H ; :: thesis: ex x being object st
( x in G & y = h . x )
then reconsider y0 = y as Element of H ;
ex x being Element of G st h . x = y0 by A2;
hence ex x being object st
( x in G & y = h . x ) ; :: thesis: verum

end;

then rng h = H by FUNCT_2:10;
hence h is onto ; :: thesis: verum