let F be Function; :: thesis: for i1, i2, xi1 being set

for Ai2 being Subset of (F . i2) st product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 holds

( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

let i1, i2, xi1 be set ; :: thesis: for Ai2 being Subset of (F . i2) st product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 holds

( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

let Ai2 be Subset of (F . i2); :: thesis: ( product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 implies ( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) ) )

assume that

A1: product F <> {} and

A2: xi1 in F . i1 and

A3: i1 in dom F and

A4: i2 in dom F and

A5: Ai2 <> F . i2 ; :: thesis: ( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

set f9 = the Element of product F;

consider f being Function such that

A6: the Element of product F = f and

A7: dom f = dom F and

for x being object st x in dom F holds

f . x in F . x by A1, CARD_3:def 5;

not F . i2 c= Ai2 by A5;

then consider xi2 being object such that

A8: xi2 in F . i2 and

A9: not xi2 in Ai2 ;

reconsider xi2 = xi2 as Element of F . i2 by A8;

A10: (f +* (i2,xi2)) . i2 = xi2 by A4, A7, FUNCT_7:31;

thus ( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 implies ( i1 = i2 & xi1 in Ai2 ) ) :: thesis: ( i1 = i2 & xi1 in Ai2 implies (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 )

A14: i1 = i2 and

A15: xi1 in Ai2 ; :: thesis: (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2

{xi1} c= Ai2 by A15, ZFMISC_1:31;

hence (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 by A14, RELAT_1:143; :: thesis: verum

for Ai2 being Subset of (F . i2) st product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 holds

( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

let i1, i2, xi1 be set ; :: thesis: for Ai2 being Subset of (F . i2) st product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 holds

( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

let Ai2 be Subset of (F . i2); :: thesis: ( product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 implies ( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) ) )

assume that

A1: product F <> {} and

A2: xi1 in F . i1 and

A3: i1 in dom F and

A4: i2 in dom F and

A5: Ai2 <> F . i2 ; :: thesis: ( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

set f9 = the Element of product F;

consider f being Function such that

A6: the Element of product F = f and

A7: dom f = dom F and

for x being object st x in dom F holds

f . x in F . x by A1, CARD_3:def 5;

not F . i2 c= Ai2 by A5;

then consider xi2 being object such that

A8: xi2 in F . i2 and

A9: not xi2 in Ai2 ;

reconsider xi2 = xi2 as Element of F . i2 by A8;

A10: (f +* (i2,xi2)) . i2 = xi2 by A4, A7, FUNCT_7:31;

thus ( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 implies ( i1 = i2 & xi1 in Ai2 ) ) :: thesis: ( i1 = i2 & xi1 in Ai2 implies (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 )

proof

assume that
assume A11:
(proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2
; :: thesis: ( i1 = i2 & xi1 in Ai2 )

thus A12: i1 = i2 :: thesis: xi1 in Ai2

then {xi1} c= rng (proj (F,i1)) by ZFMISC_1:31;

then {xi1} c= Ai2 by A11, A12, FUNCT_1:88;

hence xi1 in Ai2 by ZFMISC_1:31; :: thesis: verum

end;thus A12: i1 = i2 :: thesis: xi1 in Ai2

proof

xi1 in rng (proj (F,i1))
by A1, A2, A3, Th3;
assume A13:
i1 <> i2
; :: thesis: contradiction

( f +* (i2,xi2) in product F & (f +* (i2,xi2)) +* (i1,xi1) in (proj (F,i1)) " {xi1} ) by A1, A2, A3, A8, A6, Th2, Th5;

then f +* (i2,xi2) in (proj (F,i2)) " Ai2 by A2, A11, A13, Th6;

then ( f +* (i2,xi2) in dom (proj (F,i2)) & (proj (F,i2)) . (f +* (i2,xi2)) in Ai2 ) by FUNCT_1:def 7;

hence contradiction by A9, A10, CARD_3:def 16; :: thesis: verum

end;( f +* (i2,xi2) in product F & (f +* (i2,xi2)) +* (i1,xi1) in (proj (F,i1)) " {xi1} ) by A1, A2, A3, A8, A6, Th2, Th5;

then f +* (i2,xi2) in (proj (F,i2)) " Ai2 by A2, A11, A13, Th6;

then ( f +* (i2,xi2) in dom (proj (F,i2)) & (proj (F,i2)) . (f +* (i2,xi2)) in Ai2 ) by FUNCT_1:def 7;

hence contradiction by A9, A10, CARD_3:def 16; :: thesis: verum

then {xi1} c= rng (proj (F,i1)) by ZFMISC_1:31;

then {xi1} c= Ai2 by A11, A12, FUNCT_1:88;

hence xi1 in Ai2 by ZFMISC_1:31; :: thesis: verum

A14: i1 = i2 and

A15: xi1 in Ai2 ; :: thesis: (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2

{xi1} c= Ai2 by A15, ZFMISC_1:31;

hence (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 by A14, RELAT_1:143; :: thesis: verum