theorem Th1: :: PRALG_3:1

for f, F being Function
for A being set st f in product F holds
f | A in product (F | A)