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) )
assume A1: ( H' is normal StableSubgroup of H & K' is normal StableSubgroup of K ) ; :: thesis: H' "\/" (H /\ K') is normal StableSubgroup of H' "\/" (H /\ K)
reconsider GG = H as GroupWithOperators of O ;
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 ;
reconsider G' = H /\ K as strict StableSubgroup of GG by Lm34;
set L = H /\ K';
A2: H /\ K' is strict normal StableSubgroup of G' by A1, Th60;
then reconsider L = H /\ K' as strict StableSubgroup of GG by Th11;
A3: N = Ker f by Th48;
A4: L "\/" N = (H /\ K') "\/" H' by Th86
.= H' "\/" (H /\ K') ;
G' "\/" N = (H /\ K) "\/" H' by Th86
.= H' "\/" (H /\ K) ;
hence H' "\/" (H /\ K') is normal StableSubgroup of H' "\/" (H /\ K) by A2, A3, A4, Th90; :: thesis: verum