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