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 JK being normal StableSubgroup of K' "\/" (K /\ H) st JH = H' "\/" (H /\ K') & JK = K' "\/" (K /\ H') & H' is normal StableSubgroup of H & K' is normal StableSubgroup of K holds
(H' "\/" (H /\ K)) ./. JH,(K' "\/" (K /\ H)) ./. JK 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 JK being normal StableSubgroup of K' "\/" (K /\ H) st JH = H' "\/" (H /\ K') & JK = K' "\/" (K /\ H') & H' is normal StableSubgroup of H & K' is normal StableSubgroup of K holds
(H' "\/" (H /\ K)) ./. JH,(K' "\/" (K /\ H)) ./. JK are_isomorphic
let H, K, H', K' be strict StableSubgroup of G; :: thesis: for JH being normal StableSubgroup of H' "\/" (H /\ K)
for JK being normal StableSubgroup of K' "\/" (K /\ H) st JH = H' "\/" (H /\ K') & JK = K' "\/" (K /\ H') & H' is normal StableSubgroup of H & K' is normal StableSubgroup of K holds
(H' "\/" (H /\ K)) ./. JH,(K' "\/" (K /\ H)) ./. JK are_isomorphic
let JH be normal StableSubgroup of H' "\/" (H /\ K); :: thesis: for JK being normal StableSubgroup of K' "\/" (K /\ H) st JH = H' "\/" (H /\ K') & JK = K' "\/" (K /\ H') & H' is normal StableSubgroup of H & K' is normal StableSubgroup of K holds
(H' "\/" (H /\ K)) ./. JH,(K' "\/" (K /\ H)) ./. JK are_isomorphic
let JK be normal StableSubgroup of K' "\/" (K /\ H); :: thesis: ( JH = H' "\/" (H /\ K') & JK = K' "\/" (K /\ H') & H' is normal StableSubgroup of H & K' is normal StableSubgroup of K implies (H' "\/" (H /\ K)) ./. JH,(K' "\/" (K /\ H)) ./. JK are_isomorphic )
assume A1: ( JH = H' "\/" (H /\ K') & JK = K' "\/" (K /\ H') ) ; :: thesis: ( not H' is normal StableSubgroup of H or not K' is normal StableSubgroup of K or (H' "\/" (H /\ K)) ./. JH,(K' "\/" (K /\ H)) ./. JK are_isomorphic )
assume A2: H' is normal StableSubgroup of H ; :: thesis: ( not K' is normal StableSubgroup of K or (H' "\/" (H /\ K)) ./. JH,(K' "\/" (K /\ H)) ./. JK are_isomorphic )
assume A3: K' is normal StableSubgroup of K ; :: thesis: (H' "\/" (H /\ K)) ./. JH,(K' "\/" (K /\ H)) ./. JK are_isomorphic
set HK = (H' /\ K) "\/" (K' /\ H);
( H' /\ K is normal StableSubgroup of H /\ K & K' /\ H is normal StableSubgroup of H /\ K ) by A2, A3, Th60;
then reconsider HK = (H' /\ K) "\/" (K' /\ H) as normal StableSubgroup of H /\ K by Th87;
A4: (H' "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic by A1, A2, A3, Th91;
HK = (K' /\ H) "\/" (H' /\ K) ;
then (K' "\/" (K /\ H)) ./. JK,(H /\ K) ./. HK are_isomorphic by A1, A2, A3, Th91;
hence (H' "\/" (H /\ K)) ./. JH,(K' "\/" (K /\ H)) ./. JK are_isomorphic by A4, Th55; :: thesis: verum