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

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