for O being set
for G, H being GroupWithOperators of O
for N being StableSubgroup of G
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f holds
ex H9 being strict StableSubgroup of H st
( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )