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:36
.= f by FUNCT_7:37 ;
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