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 H' being strict normal StableSubgroup of H st
( H' <> (Omega). H & H' <> (1). H ) ) by A3, Def13;

suppose H is trivial ; :: thesis: contradiction

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

end;

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

then consider H' being strict normal StableSubgroup of H such that
A4: ( H' <> (Omega). H & H' <> (1). H ) ;
reconsider H'' = multMagma(# the carrier of H',the multF of H' #) as strict normal Subgroup of H by Lm7;
consider f being Homomorphism of G,H such that
A5: f is bijective by A1, Def22;
A6: f is onto by A5;
set A = { g where g is Element of G : f . g in H'' } ;
1_ H in H'' by GROUP_2:55;
then f . (1_ G) in H'' by Lm13;
then 1_ G in { g where g is Element of G : f . g in H'' } ;
then reconsider A = { g where g is Element of G : f . g in H'' } as non empty set ;

now

let x be set ; :: thesis: ( x in A implies x in the carrier of G )
assume x in A ; :: thesis: x in the carrier of G
then consider g being Element of G such that
A7: ( x = g & f . g in H'' ) ;
thus x in the carrier of G by A7; :: thesis: verum

end;

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

A8: now

let g1, g2 be Element of G; :: thesis: ( g1 in A & g2 in A implies g1 * g2 in A )
assume A9: ( g1 in A & g2 in A ) ; :: thesis: g1 * g2 in A
then consider a being Element of G such that
A10: ( a = g1 & f . a in H'' ) ;
consider b being Element of G such that
A11: ( b = g2 & f . b in H'' ) by A9;
A12: f . (a * b) = (f . a) * (f . b) by GROUP_6:def 7;
set fa = f . a;
set fb = f . b;
(f . a) * (f . b) in H'' by A10, A11, GROUP_2:59;
hence g1 * g2 in A by A10, A11, A12; :: thesis: verum

end;

A13: now

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
A14: ( a = g & f . a in H'' ) ;
(f . a) " in H'' by A14, GROUP_2:60;
then f . (a " ) in H'' by Lm14;
hence g " in A by A14; :: thesis: verum

end;

now

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
A15: ( a = g & f . a in H'' ) ;
f . a in the carrier of H'' by A15, STRUCT_0:def 5;
then f . a in H' by STRUCT_0:def 5;
then (H ^ o) . (f . g) in H' by A15, Lm10;
then f . ((G ^ o) . g) in H' by Def18;
then f . ((G ^ o) . g) in the carrier of H' by STRUCT_0:def 5;
then f . ((G ^ o) . g) in H'' by STRUCT_0:def 5;
hence (G ^ o) . g in A ; :: thesis: verum

end;

then consider G'' being strict StableSubgroup of G such that
A16: the carrier of G'' = A by A8, A13, Lm15;
reconsider G' = multMagma(# the carrier of G'',the multF of G'' #) as strict Subgroup of G by Lm16;
the carrier of H' <> {(1_ H)} by A4, Def8;
then consider x being set such that
A17: ( x in the carrier of H' & x <> 1_ H ) by ZFMISC_1:41;
A18: x in H'' by A17, STRUCT_0:def 5;
then x in H by GROUP_2:49;
then reconsider x = x as Element of H by STRUCT_0:def 5;
consider y being Element of G such that
A19: f . y = x by A6, Th52;
A20: y in the carrier of G'' by A16, A18, A19;
y <> 1_ G by A17, A19, Lm13;
then the carrier of G'' <> {(1_ G)} by A20, TARSKI:def 1;
then A21: G'' <> (1). G by Def8;
multMagma(# the carrier of H',the multF of H' #) <> multMagma(# the carrier of H,the multF of H #) by A4, Lm5;
then consider h being Element of H such that
A22: not h in H'' by GROUP_2:71;
consider g being Element of G such that
A23: f . g = h by A6, Th52;

now

assume g in A ; :: thesis: contradiction
then consider g' being Element of G such that
A24: ( g' = g & f . g' in H'' ) ;
thus contradiction by A22, A23, A24; :: thesis: verum

end;

then A25: G'' <> (Omega). G by A16;

now

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

now

let x be set ; :: thesis: ( x in g * G' implies x in G' * g )
assume x in g * G' ; :: thesis: x in G' * g
then consider h being Element of G such that
A26: ( x = g * h & h in A ) by A16, GROUP_2:33;
consider a being Element of G such that
A27: ( a = h & f . a in H'' ) by A26;
set h' = (g * h) * (g " );
A28: ((g * h) * (g " )) * g = (g * h) * ((g " ) * g) by GROUP_1:def 4
.= (g * h) * (1_ G) by GROUP_1:def 6
.= x by A26, GROUP_1:def 5 ;
A29: H'' |^ ((f . g) " ) = H'' by GROUP_3:def 13;
f . ((g * h) * (g " )) = (f . (g * h)) * (f . (g " )) by GROUP_6:def 7
.= ((f . g) * (f . h)) * (f . (g " )) by GROUP_6:def 7
.= ((f . g) * (f . h)) * ((f . g) " ) by Lm14
.= ((((f . g) " ) " ) * (f . h)) * ((f . g) " )
.= (f . h) |^ ((f . g) " ) by GROUP_3:def 2 ;
then f . ((g * h) * (g " )) in H'' by A27, A29, GROUP_3:70;
then (g * h) * (g " ) in A ;
hence x in G' * g by A16, A28, GROUP_2:34; :: thesis: verum

end;

hence g * G' c= G' * g by TARSKI:def 3; :: thesis: verum

end;

then for H being strict Subgroup of G st H = multMagma(# the carrier of G'',the multF of G'' #) holds
H is normal by GROUP_3:141;
then G'' is normal by Def10;
hence contradiction by A2, A21, A25, Def13; :: thesis: verum

end;

end;