:: deftheorem defines * GROUP_21:def 1 :
for I, J being non empty set
for a being Function of I,J
for G being Group
for F being Subgroup-Family of J,G holds F * a = F * a;