let F, g be Function; :: thesis: for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st i1 <> i2 & g in product F & g +* i1,xi1 in (proj F,i2) " Ai2 holds
g in (proj F,i2) " Ai2
let i1, i2, xi1 be set ; :: thesis: for Ai2 being Subset of (F . i2) st i1 <> i2 & g in product F & g +* i1,xi1 in (proj F,i2) " Ai2 holds
g in (proj F,i2) " Ai2
let Ai2 be Subset of (F . i2); :: thesis: ( i1 <> i2 & g in product F & g +* i1,xi1 in (proj F,i2) " Ai2 implies g in (proj F,i2) " Ai2 )
assume that
A1: i1 <> i2 and
A2: g in product F ; :: thesis: ( not g +* i1,xi1 in (proj F,i2) " Ai2 or g in (proj F,i2) " Ai2 )
A3: g in dom (proj F,i2) by A2, PRALG_3:def 2;
assume g +* i1,xi1 in (proj F,i2) " Ai2 ; :: thesis: g in (proj F,i2) " Ai2
then ( g +* i1,xi1 in dom (proj F,i2) & (proj F,i2) . (g +* i1,xi1) in Ai2 ) by FUNCT_1:def 13;
then (g +* i1,xi1) . i2 in Ai2 by PRALG_3:def 2;
then g . i2 in Ai2 by A1, FUNCT_7:34;
then (proj F,i2) . g in Ai2 by A3, PRALG_3:def 2;
hence g in (proj F,i2) " Ai2 by A3, FUNCT_1:def 13; :: thesis: verum