let O be set ; :: thesis: for G, H being strict GroupWithOperators of O st G,H are_isomorphic & G is simple holds
H is simple
let G, H be strict GroupWithOperators of O; :: thesis: ( G,H are_isomorphic & G is simple implies H is simple )
assume A1: G,H are_isomorphic ; :: thesis: ( not G is simple or H is simple )
assume A2: G is simple ; :: thesis: H is simple
assume A3: not H is simple ; :: thesis: contradiction

per cases ( H is trivial or ex H9 being strict normal StableSubgroup of H st
( H9 <> (Omega). H & H9 <> (1). H ) ) by A3;

suppose H is trivial ; :: thesis: contradiction

then G is trivial by A1, Th58;
hence contradiction by A2; :: thesis: verum

end;

suppose ex H9 being strict normal StableSubgroup of H st
( H9 <> (Omega). H & H9 <> (1). H ) ; :: thesis: contradiction

then consider H9 being strict normal StableSubgroup of H such that
A4: H9 <> (Omega). H and
A5: H9 <> (1). H ;
consider f being Homomorphism of G,H such that
A6: f is bijective by A1;
reconsider H99 = multMagma(# the carrier of H9, the multF of H9 #) as strict normal Subgroup of H by Lm6;
multMagma(# the carrier of H9, the multF of H9 #) <> multMagma(# the carrier of H, the multF of H #) by A4, Lm4;
then consider h being Element of H such that
A7: not h in H99 by GROUP_2:62;
the carrier of H9 <> {(1_ H)} by A5, Def8;
then consider x being object such that
A8: x in the carrier of H9 and
A9: x <> 1_ H by ZFMISC_1:35;
A10: x in H99 by A8, STRUCT_0:def 5;
then x in H by GROUP_2:40;
then reconsider x = x as Element of H by STRUCT_0:def 5;
consider y being Element of G such that
A11: f . y = x by A6, Th52;
set A = { g where g is Element of G : f . g in H99 } ;
consider g being Element of G such that
A12: f . g = h by A6, Th52;
1_ H in H99 by GROUP_2:46;
then f . (1_ G) in H99 by Lm12;
then 1_ G in { g where g is Element of G : f . g in H99 } ;
then reconsider A = { g where g is Element of G : f . g in H99 } as non empty set ;

now :: thesis: for x being object st x in A holds
x in the carrier of G

let x be object ; :: thesis: ( x in A implies x in the carrier of G )
assume x in A ; :: thesis: x in the carrier of G
then ex g being Element of G st
( x = g & f . g in H99 ) ;
hence x in the carrier of G ; :: thesis: verum

end;

then reconsider A = A as Subset of G by TARSKI:def 3;

A13: now :: thesis: for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A

let g1, g2 be Element of G; :: thesis: ( g1 in A & g2 in A implies g1 * g2 in A )
assume that
A14: g1 in A and
A15: g2 in A ; :: thesis: g1 * g2 in A
consider b being Element of G such that
A16: b = g2 and
A17: f . b in H99 by A15;
consider a being Element of G such that
A18: a = g1 and
A19: f . a in H99 by A14;
set fb = f . b;
set fa = f . a;
( f . (a * b) = (f . a) * (f . b) & (f . a) * (f . b) in H99 ) by A19, A17, GROUP_2:50, GROUP_6:def 6;
hence g1 * g2 in A by A18, A16; :: thesis: verum

end;

A20: now :: thesis: for o being Element of O
for g being Element of G st g in A holds
(G ^ o) . g in A

let o be Element of O; :: thesis: for g being Element of G st g in A holds
(G ^ o) . g in A
let g be Element of G; :: thesis: ( g in A implies (G ^ o) . g in A )
assume g in A ; :: thesis: (G ^ o) . g in A
then consider a being Element of G such that
A21: a = g and
A22: f . a in H99 ;
f . a in the carrier of H99 by A22, STRUCT_0:def 5;
then f . a in H9 by STRUCT_0:def 5;
then (H ^ o) . (f . g) in H9 by A21, Lm9;
then f . ((G ^ o) . g) in H9 by Def18;
then f . ((G ^ o) . g) in the carrier of H9 by STRUCT_0:def 5;
then f . ((G ^ o) . g) in H99 by STRUCT_0:def 5;
hence (G ^ o) . g in A ; :: thesis: verum

end;

now :: thesis: for g being Element of G st g in A holds
g " in A

let g be Element of G; :: thesis: ( g in A implies g " in A )
assume g in A ; :: thesis: g " in A
then consider a being Element of G such that
A23: a = g and
A24: f . a in H99 ;
(f . a) " in H99 by A24, GROUP_2:51;
then f . (a ") in H99 by Lm13;
hence g " in A by A23; :: thesis: verum

end;

then consider G99 being strict StableSubgroup of G such that
A25: the carrier of G99 = A by A13, A20, Lm14;
reconsider G9 = multMagma(# the carrier of G99, the multF of G99 #) as strict Subgroup of G by Lm15;

now :: thesis: for g being Element of G holds g * G9 c= G9 * g

let g be Element of G; :: thesis: g * G9 c= G9 * g

now :: thesis: for x being object st x in g * G9 holds
x in G9 * g

let x be object ; :: thesis: ( x in g * G9 implies x in G9 * g )
A26: H99 |^ ((f . g) ") = H99 by GROUP_3:def 13;
assume x in g * G9 ; :: thesis: x in G9 * g
then consider h being Element of G such that
A27: x = g * h and
A28: h in A by A25, GROUP_2:27;
set h9 = (g * h) * (g ");
A29: f . ((g * h) * (g ")) = (f . (g * h)) * (f . (g ")) by GROUP_6:def 6
.= ((f . g) * (f . h)) * (f . (g ")) by GROUP_6:def 6
.= ((((f . g) ") ") * (f . h)) * ((f . g) ") by Lm13
.= (f . h) |^ ((f . g) ") by GROUP_3:def 2 ;
ex a being Element of G st
( a = h & f . a in H99 ) by A28;
then f . ((g * h) * (g ")) in H99 by A26, A29, GROUP_3:58;
then A30: (g * h) * (g ") in A ;
((g * h) * (g ")) * g = (g * h) * ((g ") * g) by GROUP_1:def 3
.= (g * h) * (1_ G) by GROUP_1:def 5
.= x by A27, GROUP_1:def 4 ;
hence x in G9 * g by A25, A30, GROUP_2:28; :: thesis: verum

end;

hence g * G9 c= G9 * g ; :: thesis: verum

end;

then for H being strict Subgroup of G st H = multMagma(# the carrier of G99, the multF of G99 #) holds
H is normal by GROUP_3:118;
then A31: G99 is normal ;
A32: y <> 1_ G by A9, A11, Lm12;
y in the carrier of G99 by A25, A10, A11;
then the carrier of G99 <> {(1_ G)} by A32, TARSKI:def 1;
then A33: G99 <> (1). G by Def8;

now :: thesis: not g in A

assume g in A ; :: thesis: contradiction
then ex g9 being Element of G st
( g9 = g & f . g9 in H99 ) ;
hence contradiction by A7, A12; :: thesis: verum

end;

then G99 <> (Omega). G by A25;
hence contradiction by A2, A33, A31; :: thesis: verum

end;

end;