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;

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

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)

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;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

now :: thesis: for h1, h2 being Element of H holds f9 . (h1 * h2) = (f9 . h1) * (f9 . h2)

then reconsider f9 = f9 as Homomorphism of H,G by A6, Def18, GROUP_6:def 6;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;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

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