let O be set ; :: thesis: for G being GroupWithOperators of O

for H, K, H9, K9 being strict StableSubgroup of G

for JH being normal StableSubgroup of H9 "\/" (H /\ K)

for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds

(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

let G be GroupWithOperators of O; :: thesis: for H, K, H9, K9 being strict StableSubgroup of G

for JH being normal StableSubgroup of H9 "\/" (H /\ K)

for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds

(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

let H, K, H9, K9 be strict StableSubgroup of G; :: thesis: for JH being normal StableSubgroup of H9 "\/" (H /\ K)

for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds

(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

reconsider GG = H as GroupWithOperators of O ;

set G9 = H /\ K;

set L = H /\ K9;

reconsider G9 = H /\ K as strict StableSubgroup of GG by Lm33;

let JH be normal StableSubgroup of H9 "\/" (H /\ K); :: thesis: for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds

(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

let HK be normal StableSubgroup of H /\ K; :: thesis: ( H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) implies (H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic )

assume that

A1: H9 is normal StableSubgroup of H and

A2: K9 is normal StableSubgroup of K ; :: thesis: ( not JH = H9 "\/" (H /\ K9) or not HK = (H9 /\ K) "\/" (K9 /\ H) or (H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic )

A3: H /\ K9 is normal StableSubgroup of G9 by A2, Th60;

reconsider N9 = H9 as normal StableSubgroup of GG by A1;

assume that

A4: JH = H9 "\/" (H /\ K9) and

A5: HK = (H9 /\ K) "\/" (K9 /\ H) ; :: thesis: (H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

reconsider N = N9 as StableSubgroup of GG ;

set N1 = G9 /\ N;

A6: G9 "\/" N = (H /\ K) "\/" H9 by Th86

.= H9 "\/" (H /\ K) ;

reconsider L = H /\ K9 as StableSubgroup of GG by A3, Th11;

G9 /\ N = (H /\ K) /\ H9 by Th39;

then A7: L "\/" (G9 /\ N) = (H /\ K9) "\/" ((H /\ K) /\ H9) by Th86

.= ((H9 /\ H) /\ K) "\/" (K9 /\ H) by Th20

.= HK by A1, A5, Lm21 ;

reconsider HH = GG ./. N9 as GroupWithOperators of O ;

reconsider f = nat_hom N9 as Homomorphism of GG,HH ;

A8: N = Ker f by Th48;

L "\/" N = (H /\ K9) "\/" H9 by Th86

.= JH by A4 ;

hence (H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic by A3, A7, A8, A6, Th90; :: thesis: verum

for H, K, H9, K9 being strict StableSubgroup of G

for JH being normal StableSubgroup of H9 "\/" (H /\ K)

for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds

(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

let G be GroupWithOperators of O; :: thesis: for H, K, H9, K9 being strict StableSubgroup of G

for JH being normal StableSubgroup of H9 "\/" (H /\ K)

for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds

(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

let H, K, H9, K9 be strict StableSubgroup of G; :: thesis: for JH being normal StableSubgroup of H9 "\/" (H /\ K)

for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds

(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

reconsider GG = H as GroupWithOperators of O ;

set G9 = H /\ K;

set L = H /\ K9;

reconsider G9 = H /\ K as strict StableSubgroup of GG by Lm33;

let JH be normal StableSubgroup of H9 "\/" (H /\ K); :: thesis: for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds

(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

let HK be normal StableSubgroup of H /\ K; :: thesis: ( H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) implies (H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic )

assume that

A1: H9 is normal StableSubgroup of H and

A2: K9 is normal StableSubgroup of K ; :: thesis: ( not JH = H9 "\/" (H /\ K9) or not HK = (H9 /\ K) "\/" (K9 /\ H) or (H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic )

A3: H /\ K9 is normal StableSubgroup of G9 by A2, Th60;

reconsider N9 = H9 as normal StableSubgroup of GG by A1;

assume that

A4: JH = H9 "\/" (H /\ K9) and

A5: HK = (H9 /\ K) "\/" (K9 /\ H) ; :: thesis: (H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

reconsider N = N9 as StableSubgroup of GG ;

set N1 = G9 /\ N;

A6: G9 "\/" N = (H /\ K) "\/" H9 by Th86

.= H9 "\/" (H /\ K) ;

reconsider L = H /\ K9 as StableSubgroup of GG by A3, Th11;

G9 /\ N = (H /\ K) /\ H9 by Th39;

then A7: L "\/" (G9 /\ N) = (H /\ K9) "\/" ((H /\ K) /\ H9) by Th86

.= ((H9 /\ H) /\ K) "\/" (K9 /\ H) by Th20

.= HK by A1, A5, Lm21 ;

reconsider HH = GG ./. N9 as GroupWithOperators of O ;

reconsider f = nat_hom N9 as Homomorphism of GG,HH ;

A8: N = Ker f by Th48;

L "\/" N = (H /\ K9) "\/" H9 by Th86

.= JH by A4 ;

hence (H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic by A3, A7, A8, A6, Th90; :: thesis: verum