let O be set ; :: thesis: for G, H being GroupWithOperators of O st G,H are_isomorphic holds
H,G are_isomorphic
let G, H be GroupWithOperators of O; :: thesis: ( G,H are_isomorphic implies H,G are_isomorphic )
assume G,H are_isomorphic ; :: thesis: H,G are_isomorphic
then consider f being Homomorphism of G,H such that
A1: f is bijective by Def22;
( f is onto & f is one-to-one ) by A1;
then A2: ( rng f = the carrier of H & f is one-to-one ) by FUNCT_2:def 3;
A3: dom f = the carrier of G by FUNCT_2:def 1;
set f' = f " ;
A4: ( dom (f " ) = the carrier of H & rng (f " ) = the carrier of G ) by A2, A3, FUNCT_1:55;
then reconsider f' = f " as Function of H,G by FUNCT_2:3;

A5: now

let h1, h2 be Element of H; :: thesis: f' . (h1 * h2) = (f' . h1) * (f' . h2)
set g1 = f' . h1;
set g2 = f' . h2;
( f . (f' . h1) = h1 & f . (f' . h2) = h2 ) by A2, FUNCT_1:57;
hence f' . (h1 * h2) = f' . (f . ((f' . h1) * (f' . h2))) by GROUP_6:def 7
.= (f' . h1) * (f' . h2) by A2, A3, FUNCT_1:56 ;
:: thesis: verum

end;

now

let o be Element of O; :: thesis: for h being Element of H holds f' . ((H ^ o) . h) = (G ^ o) . (f' . h)
let h be Element of H; :: thesis: f' . ((H ^ o) . h) = (G ^ o) . (f' . h)
set g = f' . h;
thus f' . ((H ^ o) . h) = f' . ((H ^ o) . (f . (f' . h))) by A2, FUNCT_1:57
.= f' . (f . ((G ^ o) . (f' . h))) by Def18
.= (G ^ o) . (f' . h) by A2, A3, FUNCT_1:56 ; :: thesis: verum

end;

then reconsider f' = f' as Homomorphism of H,G by A5, Def18, GROUP_6:def 7;
f' is one-to-one by A2;
then A6: ( f' is onto & f' is one-to-one ) by A4, FUNCT_2:def 3;
take f' ; :: according to GROUP_9:def 22 :: thesis: f' is bijective
thus f' is bijective by A6; :: thesis: verum