theorem Th84: :: GROUP_9:84

for O, E1, E2 being set
for A1 being Action of O,E1
for A2 being Action of O,E2
for F being FinSequence of O st E1 c= E2 & ( for o being Element of O
for f1 being Function of E1,E1
for f2 being Function of E2,E2 st f1 = A1 . o & f2 = A2 . o holds
f1 = f2 | E1 ) holds
Product (F,A1) = (Product (F,A2)) | E1