let G, H be Group; :: thesis: for c being Element of H
for h being Homomorphism of G,H st h is one-to-one & c in Image h holds
h . ((h ") . c) = c
let c be Element of H; :: thesis: for h being Homomorphism of G,H st h is one-to-one & c in Image h holds
h . ((h ") . c) = c
let h be Homomorphism of G,H; :: thesis: ( h is one-to-one & c in Image h implies h . ((h ") . c) = c )
reconsider h9 = h as Function of G,(Image h) by Th49;
assume that
A1: h is one-to-one and
A2: c in Image h ; :: thesis: h . ((h ") . c) = c
A3: rng h9 = the carrier of (Image h) by Th44;
c in the carrier of (Image h) by A2;
hence h . ((h ") . c) = c by A1, A3, FUNCT_1:35; :: thesis: verum