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

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