let G be GroupWithOperators of O; :: thesis: ex h being Homomorphism of G,G st h is bijective

reconsider G9 = G as Group ;

set h = id the carrier of G9;

for o being Element of O

for g being Element of G holds (id the carrier of G9) . ((G ^ o) . g) = (G ^ o) . ((id the carrier of G9) . g) ;

then reconsider h = id the carrier of G9 as Homomorphism of G,G by Def18, GROUP_6:38;

take h ; :: thesis: h is bijective

h is onto ;

hence h is bijective ; :: thesis: verum

reconsider G9 = G as Group ;

set h = id the carrier of G9;

for o being Element of O

for g being Element of G holds (id the carrier of G9) . ((G ^ o) . g) = (G ^ o) . ((id the carrier of G9) . g) ;

then reconsider h = id the carrier of G9 as Homomorphism of G,G by Def18, GROUP_6:38;

take h ; :: thesis: h is bijective

h is onto ;

hence h is bijective ; :: thesis: verum