:: deftheorem Def22 defines Image GROUP_9:def 22 :
for O being set
for G, H being GroupWithOperators of O
for g being Homomorphism of G,H
for b₅ being strict StableSubgroup of H holds
( b₅ = Image g iff the carrier of b₅ = g .: the carrier of G );