let F, f be Function; :: thesis: 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 )
let i1, i2, xi1 be set ; :: thesis: 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 )
let Ai2 be Subset of (F . i2); :: thesis: ( xi1 in F . i1 & f in product F & i1 <> i2 implies ( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 ) )
assume that
A1: xi1 in F . i1 and
A2: f in product F ; :: thesis: ( not i1 <> i2 or ( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 ) )
assume A3: i1 <> i2 ; :: thesis: ( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 )
thus ( f in (proj (F,i2)) " Ai2 implies f +* (i1,xi1) in (proj (F,i2)) " Ai2 ) :: thesis: ( f +* (i1,xi1) in (proj (F,i2)) " Ai2 implies f in (proj (F,i2)) " Ai2 )

proof

A4: (f +* (i1,xi1)) +* (i1,(f . i1)) = f +* (i1,(f . i1)) by FUNCT_7:34
.= f by FUNCT_7:35 ;
assume f in (proj (F,i2)) " Ai2 ; :: thesis: f +* (i1,xi1) in (proj (F,i2)) " Ai2
hence f +* (i1,xi1) in (proj (F,i2)) " Ai2 by A1, A2, A3, A4, Lm1, Th2; :: thesis: verum

end;

assume f +* (i1,xi1) in (proj (F,i2)) " Ai2 ; :: thesis: f in (proj (F,i2)) " Ai2
hence f in (proj (F,i2)) " Ai2 by A2, A3, Lm1; :: thesis: verum