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