:: deftheorem Def3 defines characteristic GROUP_22:def 4 :
for G being Group
for IT being Subgroup of G holds
( IT is characteristic iff for f being Automorphism of G holds Image (f | IT) = multMagma(# the carrier of IT, the multF of IT #) );