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 <> {} & xi1 in F . i1 )
and
A2:
i1 in dom F
and
A3:
i2 in dom F
and
A4:
Ai2 <> F . i2
; :: thesis: ( (proj F,i1) " {xi1} c= (proj F,i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
not F . i2 c= Ai2
by A4, XBOOLE_0:def 10;
then consider xi2 being set such that
A5:
xi2 in F . i2
and
A6:
not xi2 in Ai2
by TARSKI:def 3;
reconsider xi2 = xi2 as Element of F . i2 by A5;
consider f' being Element of product F;
consider f being Function such that
A7:
f' = f
and
A8:
dom f = dom F
and
for x being set st x in dom F holds
f . x in F . x
by A1, CARD_3:def 5;
A9:
(f +* i2,xi2) . i2 = xi2
by A3, A8, FUNCT_7:33;
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 A10:
(proj F,i1) " {xi1} c= (proj F,i2) " Ai2
;
:: thesis: ( i1 = i2 & xi1 in Ai2 )
thus A11:
i1 = i2
:: thesis: xi1 in Ai2proof
assume A12:
i1 <> i2
;
:: thesis: contradiction
A13:
f +* i2,
xi2 in product F
by A1, A5, A7, Th2;
(f +* i2,xi2) +* i1,
xi1 in (proj F,i1) " {xi1}
by A1, A2, A5, A7, Th2, Th5;
then
f +* i2,
xi2 in (proj F,i2) " Ai2
by A1, A2, A10, A12, A13, Th6;
then
(
f +* i2,
xi2 in dom (proj F,i2) &
(proj F,i2) . (f +* i2,xi2) in Ai2 )
by FUNCT_1:def 13;
hence
contradiction
by A6, A9, PRALG_3:def 2;
:: thesis: verum
end;
xi1 in rng (proj F,i1)
by A1, A2, Th3;
then
{xi1} c= rng (proj F,i1)
by ZFMISC_1:37;
then
{xi1} c= Ai2
by A10, A11, FUNCT_1:158;
hence
xi1 in Ai2
by ZFMISC_1:37;
:: 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:37;
hence
(proj F,i1) " {xi1} c= (proj F,i2) " Ai2
by A14, RELAT_1:178; :: thesis: verum