theorem Th6: :: YELLOW17:6

for F, f being Function
for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st xi1 in F . i1 & f in product F & i1 <> i2 holds
( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 )