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 JK being normal StableSubgroup of K9 "\/" (K /\ H) st JH = H9 "\/" (H /\ K9) & JK = K9 "\/" (K /\ H9) & H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds

(H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK 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 JK being normal StableSubgroup of K9 "\/" (K /\ H) st JH = H9 "\/" (H /\ K9) & JK = K9 "\/" (K /\ H9) & H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds

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

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

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

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

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

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

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

assume that

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

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

set HK = (H9 /\ K) "\/" (K9 /\ H);

assume A3: H9 is normal StableSubgroup of H ; :: thesis: ( not K9 is normal StableSubgroup of K or (H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK are_isomorphic )

then A4: H9 /\ K is normal StableSubgroup of H /\ K by Th60;

assume A5: K9 is normal StableSubgroup of K ; :: thesis: (H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK are_isomorphic

then K9 /\ H is normal StableSubgroup of H /\ K by Th60;

then reconsider HK = (H9 /\ K) "\/" (K9 /\ H) as normal StableSubgroup of H /\ K by A4, Th87;

HK = (K9 /\ H) "\/" (H9 /\ K) ;

then A6: (K9 "\/" (K /\ H)) ./. JK,(H /\ K) ./. HK are_isomorphic by A2, A3, A5, Th91;

(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic by A1, A3, A5, Th91;

hence (H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK are_isomorphic by A6, Th55; :: thesis: verum

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

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

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

(H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK 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 JK being normal StableSubgroup of K9 "\/" (K /\ H) st JH = H9 "\/" (H /\ K9) & JK = K9 "\/" (K /\ H9) & H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds

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

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

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

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

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

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

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

assume that

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

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

set HK = (H9 /\ K) "\/" (K9 /\ H);

assume A3: H9 is normal StableSubgroup of H ; :: thesis: ( not K9 is normal StableSubgroup of K or (H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK are_isomorphic )

then A4: H9 /\ K is normal StableSubgroup of H /\ K by Th60;

assume A5: K9 is normal StableSubgroup of K ; :: thesis: (H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK are_isomorphic

then K9 /\ H is normal StableSubgroup of H /\ K by Th60;

then reconsider HK = (H9 /\ K) "\/" (K9 /\ H) as normal StableSubgroup of H /\ K by A4, Th87;

HK = (K9 /\ H) "\/" (H9 /\ K) ;

then A6: (K9 "\/" (K /\ H)) ./. JK,(H /\ K) ./. HK are_isomorphic by A2, A3, A5, Th91;

(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic by A1, A3, A5, Th91;

hence (H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK are_isomorphic by A6, Th55; :: thesis: verum