:: deftheorem defines distributive GROUP_9:def 4 :
for O being set
for G being Group
for IT being Action of O, the carrier of G holds
( IT is distributive iff for o being Element of O st o in O holds
IT . o is Homomorphism of G,G );