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