:: deftheorem Def13 defines normal GROUP_3:def 13 :
for G being Group
for IT being Subgroup of G holds
( IT is normal iff for a being Element of G holds IT |^ a = multMagma(# the carrier of IT, the multF of IT #) );