let O be set ; for G being GroupWithOperators of O
for H, K, H9, K9 being strict StableSubgroup of G st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds
H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)
let G be GroupWithOperators of O; for H, K, H9, K9 being strict StableSubgroup of G st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds
H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)
let H, K, H9, K9 be strict StableSubgroup of G; ( H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K implies H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K) )
reconsider GG = H as GroupWithOperators of O ;
reconsider G9 = H /\ K as strict StableSubgroup of GG by Lm33;
assume that
A1:
H9 is normal StableSubgroup of H
and
A2:
K9 is normal StableSubgroup of K
; H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)
reconsider N9 = H9 as normal StableSubgroup of GG by A1;
reconsider N = N9 as StableSubgroup of GG ;
reconsider HH = GG ./. N9 as GroupWithOperators of O ;
reconsider f = nat_hom N9 as Homomorphism of GG,HH ;
set L = H /\ K9;
A3:
H /\ K9 is strict normal StableSubgroup of G9
by A2, Th60;
then reconsider L = H /\ K9 as strict StableSubgroup of GG by Th11;
A4:
N = Ker f
by Th48;
A5: G9 "\/" N =
(H /\ K) "\/" H9
by Th86
.=
H9 "\/" (H /\ K)
;
L "\/" N =
(H /\ K9) "\/" H9
by Th86
.=
H9 "\/" (H /\ K9)
;
hence
H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)
by A3, A4, A5, Th90; verum