let G1, G2 be Group; :: thesis: ( G1,G2 are_isomorphic implies center G1, center G2 are_isomorphic )
assume G1,G2 are_isomorphic ; :: thesis: center G1, center G2 are_isomorphic
then consider phi being Homomorphism of G1,G2 such that
A1: phi is bijective by GROUP_6:def 11;
ex psi being Homomorphism of (center G1),(center G2) st psi is bijective

proof

set U1 = the carrier of (center G1);
set U2 = the carrier of (center G2);
A2: phi | the carrier of (center G1) is one-to-one by A1, FUNCT_1:52;
the carrier of (center G1) c= the carrier of G1 by GROUP_2:def 5;
then phi | the carrier of (center G1) is Function of the carrier of (center G1),G2 by FUNCT_2:32;
then A3: dom (phi | the carrier of (center G1)) = the carrier of (center G1) by FUNCT_2:def 1;
A4: rng (phi | the carrier of (center G1)) = the carrier of (center G2)

proof

now :: thesis: for y being object st y in rng (phi | the carrier of (center G1)) holds
y in the carrier of (center G2)

let y be object ; :: thesis: ( y in rng (phi | the carrier of (center G1)) implies y in the carrier of (center G2) )
assume A5: y in rng (phi | the carrier of (center G1)) ; :: thesis: y in the carrier of (center G2)
then reconsider y9 = y as Element of G2 ;
consider x being object such that
A6: ( x in dom (phi | the carrier of (center G1)) & y = (phi | the carrier of (center G1)) . x ) by A5, FUNCT_1:def 3;
reconsider x9 = x as Element of G1 by A6;
for z9 being Element of G2 holds z9 * y9 = y9 * z9

proof

let z9 be Element of G2; :: thesis: z9 * y9 = y9 * z9
rng phi = the carrier of G2 by A1, FUNCT_2:def 3;
then consider w being object such that
A7: ( w in dom phi & z9 = phi . w ) by FUNCT_1:def 3;
reconsider w9 = w as Element of G1 by A7;
A8: ( y9 = phi . x9 & z9 = phi . w9 ) by A3, A6, A7, FUNCT_1:49;
hence z9 * y9 = phi . (w9 * x9) by GROUP_6:def 6
.= phi . (x9 * w9) by A3, A6, GROUP_5:77, STRUCT_0:def 5
.= y9 * z9 by A8, GROUP_6:def 6 ;
:: thesis: verum

end;

hence y in the carrier of (center G2) by GROUP_5:77, STRUCT_0:def 5; :: thesis: verum

end;

then A9: rng (phi | the carrier of (center G1)) c= the carrier of (center G2) by TARSKI:def 3;

now :: thesis: for y being object st y in the carrier of (center G2) holds
y in rng (phi | the carrier of (center G1))

let y be object ; :: thesis: ( y in the carrier of (center G2) implies y in rng (phi | the carrier of (center G1)) )
assume A10: y in the carrier of (center G2) ; :: thesis: y in rng (phi | the carrier of (center G1))
A11: rng phi = the carrier of G2 by A1, FUNCT_2:def 3;
y in center G2 by A10, STRUCT_0:def 5;
then reconsider y9 = y as Element of G2 by GROUP_2:40, STRUCT_0:def 5;
( y = y9 & y9 in the carrier of G2 ) ;
then consider x being object such that
A12: ( x in dom phi & y = phi . x ) by A11, FUNCT_1:def 3;
reconsider x9 = x as Element of G1 by A12;
A13: phi is one-to-one by A1;
A14: phi . x9 in center G2 by A10, A12, STRUCT_0:def 5;
for w9 being Element of G1 holds x9 * w9 = w9 * x9

proof

let w9 be Element of G1; :: thesis: x9 * w9 = w9 * x9
A15: dom phi = the carrier of G1 by FUNCT_2:def 1;
hence x9 * w9 = (phi ") . (phi . (x9 * w9)) by A13, FUNCT_1:34
.= (phi ") . ((phi . x9) * (phi . w9)) by GROUP_6:def 6
.= (phi ") . ((phi . w9) * (phi . x9)) by A14, GROUP_5:77
.= (phi ") . (phi . (w9 * x9)) by GROUP_6:def 6
.= w9 * x9 by A13, A15, FUNCT_1:34 ;
:: thesis: verum

end;

then x9 in the carrier of (center G1) by GROUP_5:77, STRUCT_0:def 5;
hence y in rng (phi | the carrier of (center G1)) by A12, FUNCT_1:50; :: thesis: verum

end;

then the carrier of (center G2) c= rng (phi | the carrier of (center G1)) by TARSKI:def 3;
hence rng (phi | the carrier of (center G1)) = the carrier of (center G2) by A9, XBOOLE_0:def 10; :: thesis: verum

end;

then reconsider psi = phi | the carrier of (center G1) as Function of (center G1),(center G2) by A3, FUNCT_2:2;
for a, b being Element of (center G1) holds psi . (a * b) = (psi . a) * (psi . b)

proof

let a, b be Element of (center G1); :: thesis: psi . (a * b) = (psi . a) * (psi . b)
reconsider x = a, y = b as Element of G1 by GROUP_2:42;
A16: psi . a = phi . x by FUNCT_1:49;
A17: psi . b = phi . y by FUNCT_1:49;
thus psi . (a * b) = phi . (a * b) by FUNCT_1:49
.= phi . (x * y) by GROUP_2:43
.= (phi . x) * (phi . y) by GROUP_6:def 6
.= (psi . a) * (psi . b) by A16, A17, GROUP_2:43 ; :: thesis: verum

end;

then reconsider psi = psi as Homomorphism of (center G1),(center G2) by GROUP_6:def 6;
take psi ; :: thesis: psi is bijective
psi is onto by A4, FUNCT_2:def 3;
hence psi is bijective by A2; :: thesis: verum

end;

hence center G1, center G2 are_isomorphic by GROUP_6:def 11; :: thesis: verum