for O being set
for G, H being GroupWithOperators of O
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9 by Lm16;