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 )
proof
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
proof
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;
xi1 in rng (proj (F,i1)) by A1, A2, A3, Th3;
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;
assume that
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