let O be set ; :: thesis: for G being GroupWithOperators of O
for H being strict GroupWithOperators of O
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 G be GroupWithOperators of O; :: thesis: for H being strict GroupWithOperators of O
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 GroupWithOperators of O; :: 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 A1: h is onto ; :: 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
rng h = the carrier of H by A1;
then consider a being object such that
A2: a in dom h and
A3: c = h . a by FUNCT_1:def 3;
reconsider a = a as Element of G by A2;
take a ; :: thesis: h . a = c
thus h . a = c by A3; :: thesis: verum