theorem :: GROUP_9:64

for O being non empty set
for E being set
for F1, F2 being FinSequence of O
for A being Action of O,E holds Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A)) by Lm28;