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;

now

let o be Element of O; :: thesis: for g being Element of G holds (id the carrier of G9) . ((G ^ o) . g) = (G ^ o) . ((id the carrier of G9) . g)
let g be Element of G; :: thesis: (id the carrier of G9) . ((G ^ o) . g) = (G ^ o) . ((id the carrier of G9) . g)
(id the carrier of G9) . ((G ^ o) . g) = (G ^ o) . g by FUNCT_1:34;
hence (id the carrier of G9) . ((G ^ o) . g) = (G ^ o) . ((id the carrier of G9) . g) by FUNCT_1:34; :: thesis: verum

end;

then reconsider h = id the carrier of G9 as Homomorphism of G,G by Def18, GROUP_6:47;
take h ; :: thesis: h is bijective
rng h = the carrier of G by RELAT_1:71;
then h is onto by FUNCT_2:def 3;
hence h is bijective ; :: thesis: verum