let G be Group; :: thesis: for H being strict Group
for h being Homomorphism 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 strict Group; :: thesis: for h being Homomorphism 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 Homomorphism 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 h is onto ; :: thesis: for c being Element of H ex a being Element of G st h . a = c
then A1: Image h = H by Th67;

now

let c be Element of H; :: thesis: ex a being Element of G st h . a = c
c in Image h by A1, STRUCT_0:def 5;
hence ex a being Element of G st h . a = c by Th54; :: thesis: verum

end;

hence for c being Element of H ex a being Element of G st h . a = c ; :: thesis: verum