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, CARD_3:def 16;
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 7;
then (g +* (i1,xi1)) . i2 in Ai2 by CARD_3:def 16;
then g . i2 in Ai2 by A1, FUNCT_7:32;
then (proj (F,i2)) . g in Ai2 by A3, CARD_3:def 16;
hence g in (proj (F,i2)) " Ai2 by A3, FUNCT_1:def 7; :: thesis: verum