theorem :: GROUP_9:63

for O being non empty set
for E being set
for o being Element of O
for A being Action of O,E holds Product (<*o*>,A) = A . o by Lm25;