let G be GroupWithOperators of O; :: thesis: ex h being Homomorphism of G,G st h is bijective
reconsider G' = G as Group ;
set h = id the carrier of G';

now

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

end;

then reconsider h = id the carrier of G' 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