theorem Th2: :: YELLOW17:2

for F, f being Function
for i, xi being set st xi in F . i & f in product F holds
f +* (i,xi) in product F