:: deftheorem Def5 defines distributive GROUP_9:def 5 :
for O being set
for IT being non empty HGrWOpStr over O holds
( IT is distributive iff for G being Group
for a being Action of O, the carrier of G st a = the action of IT & multMagma(# the carrier of G, the multF of G #) = multMagma(# the carrier of IT, the multF of IT #) holds
a is distributive );