let O be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 Lm34;
assume that
A1: H9 is normal StableSubgroup of H and
A2: K9 is normal StableSubgroup of K ; :: thesis: 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; :: thesis: verum