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 ;
set f9 = f " ;
A2: rng f = the carrier of H by A1, FUNCT_2:def 3;
then A3: dom (f ") = the carrier of H by A1, FUNCT_1:33;
A4: dom f = the carrier of G by FUNCT_2:def 1;
then A5: rng (f ") = the carrier of G by A1, FUNCT_1:33;
then reconsider f9 = f " as Function of H,G by A3, FUNCT_2:1;
A6: now :: thesis: for o being Element of O
for h being Element of H holds f9 . ((H ^ o) . h) = (G ^ o) . (f9 . h)
let o be Element of O; :: thesis: for h being Element of H holds f9 . ((H ^ o) . h) = (G ^ o) . (f9 . h)
let h be Element of H; :: thesis: f9 . ((H ^ o) . h) = (G ^ o) . (f9 . h)
set g = f9 . h;
thus f9 . ((H ^ o) . h) = f9 . ((H ^ o) . (f . (f9 . h))) by A1, A2, FUNCT_1:35
.= f9 . (f . ((G ^ o) . (f9 . h))) by Def18
.= (G ^ o) . (f9 . h) by A1, A4, FUNCT_1:34 ; :: thesis: verum
end;
now :: thesis: for h1, h2 being Element of H holds f9 . (h1 * h2) = (f9 . h1) * (f9 . h2)
let h1, h2 be Element of H; :: thesis: f9 . (h1 * h2) = (f9 . h1) * (f9 . h2)
set g1 = f9 . h1;
set g2 = f9 . h2;
( f . (f9 . h1) = h1 & f . (f9 . h2) = h2 ) by A1, A2, FUNCT_1:35;
hence f9 . (h1 * h2) = f9 . (f . ((f9 . h1) * (f9 . h2))) by GROUP_6:def 6
.= (f9 . h1) * (f9 . h2) by A1, A4, FUNCT_1:34 ;
:: thesis: verum
end;
then reconsider f9 = f9 as Homomorphism of H,G by A6, Def18, GROUP_6:def 6;
take f9 ; :: according to GROUP_9:def 19 :: thesis: f9 is bijective
f9 is onto by A5;
hence f9 is bijective by A1; :: thesis: verum