theorem Th5: :: YELLOW17:5

for F, f being Function
for i, xi being set st xi in F . i & i in dom F & f in product F holds
f +* (i,xi) in (proj (F,i)) " {xi}