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

for H, K, H9, K9 being strict StableSubgroup of G st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds

H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)

let G be GroupWithOperators of O; :: thesis: for H, K, H9, K9 being strict StableSubgroup of G st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds

H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)

let H, K, H9, K9 be strict StableSubgroup of G; :: thesis: ( H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K implies H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K) )

reconsider GG = H as GroupWithOperators of O ;

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

assume that

A1: H9 is normal StableSubgroup of H and

A2: K9 is normal StableSubgroup of K ; :: thesis: H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)

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

reconsider N = N9 as StableSubgroup of GG ;

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

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

set L = H /\ K9;

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

then reconsider L = H /\ K9 as strict StableSubgroup of GG by Th11;

A4: N = Ker f by Th48;

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

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

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

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

hence H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K) by A3, A4, A5, Th90; :: thesis: verum

for H, K, H9, K9 being strict StableSubgroup of G st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds

H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)

let G be GroupWithOperators of O; :: thesis: for H, K, H9, K9 being strict StableSubgroup of G st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds

H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)

let H, K, H9, K9 be strict StableSubgroup of G; :: thesis: ( H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K implies H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K) )

reconsider GG = H as GroupWithOperators of O ;

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

assume that

A1: H9 is normal StableSubgroup of H and

A2: K9 is normal StableSubgroup of K ; :: thesis: H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)

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

reconsider N = N9 as StableSubgroup of GG ;

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

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

set L = H /\ K9;

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

then reconsider L = H /\ K9 as strict StableSubgroup of GG by Th11;

A4: N = Ker f by Th48;

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

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

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

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

hence H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K) by A3, A4, A5, Th90; :: thesis: verum