theorem Th4: :: YELLOW17:4

for F being Function
for i being set st i in dom F holds
(proj (F,i)) " (F . i) = product F