let G, H be non empty set ; :: thesis: for h being Function of G,H st h is onto holds
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 implies for c being Element of H ex a being Element of G st h . a = c )
assume A1: rng h = H ; :: according to FUNCT_2:def 3 :: thesis: for c being Element of H ex a being Element of G st h . a = c
let c be Element of H; :: thesis: ex a being Element of G st h . a = c
ex a being set 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