for O being set
for G, H being strict GroupWithOperators of O
for N, L, G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f & L is strict normal StableSubgroup of G9 holds
( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )