let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being Subset of (product (Carrier J))
for i, j being Element of I st i <> j & ex F being ManySortedSet of I st
( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) ) holds
<:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):]
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for P being Subset of (product (Carrier J))
for i, j being Element of I st i <> j & ex F being ManySortedSet of I st
( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) ) holds
<:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):]
let P be Subset of (product (Carrier J)); :: thesis: for i, j being Element of I st i <> j & ex F being ManySortedSet of I st
( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) ) holds
<:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):]
let i, j be Element of I; :: thesis: ( i <> j & ex F being ManySortedSet of I st
( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) ) implies <:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):] )
assume that
A1: i <> j and
A2: ex F being ManySortedSet of I st
( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) ) ; :: thesis: <:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):]
consider F being ManySortedSet of I such that
A3: P = product F and
A4: for k being Element of I holds F . k c= (Carrier J) . k by A2;

per cases ( F is non-empty or not F is non-empty ) ;

suppose A5: F is non-empty ; :: thesis: <:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):]

for y being object st y in [:((proj (J,i)) .: P),((proj (J,j)) .: P):] holds
y in <:(proj (J,i)),(proj (J,j)):> .: P

proof

let y be object ; :: thesis: ( y in [:((proj (J,i)) .: P),((proj (J,j)) .: P):] implies y in <:(proj (J,i)),(proj (J,j)):> .: P )
assume y in [:((proj (J,i)) .: P),((proj (J,j)) .: P):] ; :: thesis: y in <:(proj (J,i)),(proj (J,j)):> .: P
then consider y1, y2 being object such that
A6: ( y1 in (proj (J,i)) .: P & y2 in (proj (J,j)) .: P & y = [y1,y2] ) by ZFMISC_1:def 2;
A7: dom F = I by PARTFUN1:def 2
.= dom (Carrier J) by PARTFUN1:def 2 ;
( i in I & j in I ) ;
then A8: ( i in dom F & j in dom F ) by PARTFUN1:def 2;
for k being object st k in dom F holds
F . k c= (Carrier J) . k by A4;
then ( (proj ((Carrier J),i)) .: P = F . i & (proj ((Carrier J),j)) .: P = F . j ) by A3, A5, A7, A8, Th26;
then A9: ( (proj (J,i)) .: P = F . i & (proj (J,j)) .: P = F . j ) by WAYBEL18:def 4;
set p0 = the Element of product F;
set p = the Element of product F +* ((i,j) --> (y1,y2));
A10: dom <:(proj (J,i)),(proj (J,j)):> = (dom (proj (J,i))) /\ (dom (proj (J,j))) by FUNCT_3:def 7
.= (dom (proj ((Carrier J),i))) /\ (dom (proj (J,j))) by WAYBEL18:def 4
.= (dom (proj ((Carrier J),i))) /\ (dom (proj ((Carrier J),j))) by WAYBEL18:def 4 ;
then A11: dom <:(proj (J,i)),(proj (J,j)):> = (dom (proj ((Carrier J),i))) /\ (product (Carrier J)) by CARD_3:def 16
.= (product (Carrier J)) /\ (product (Carrier J)) by CARD_3:def 16
.= product (Carrier J) ;
the Element of product F +* ((i,j) --> (y1,y2)) in product (F +* ((i,j) --> ((F . i),(F . j)))) by A1, A6, A5, A9, Th30;
then A12: the Element of product F +* ((i,j) --> (y1,y2)) in P by A3, A8, Th11;
then A14: ( the Element of product F +* ((i,j) --> (y1,y2)) in dom (proj ((Carrier J),i)) & the Element of product F +* ((i,j) --> (y1,y2)) in dom (proj ((Carrier J),j)) ) by A11, A10, XBOOLE_0:def 4;
A15: (proj (J,i)) . ( the Element of product F +* ((i,j) --> (y1,y2))) = (proj ((Carrier J),i)) . ( the Element of product F +* ((i,j) --> (y1,y2))) by WAYBEL18:def 4
.= ( the Element of product F +* ((i,j) --> (y1,y2))) . i by A14, CARD_3:def 16
.= y1 by A1, FUNCT_4:84 ;
A16: (proj (J,j)) . ( the Element of product F +* ((i,j) --> (y1,y2))) = (proj ((Carrier J),j)) . ( the Element of product F +* ((i,j) --> (y1,y2))) by WAYBEL18:def 4
.= ( the Element of product F +* ((i,j) --> (y1,y2))) . j by A14, CARD_3:def 16
.= y2 by A1, FUNCT_4:84 ;
<:(proj (J,i)),(proj (J,j)):> . ( the Element of product F +* ((i,j) --> (y1,y2))) = [y1,y2] by A11, A12, A15, A16, FUNCT_3:def 7;
hence y in <:(proj (J,i)),(proj (J,j)):> .: P by A6, A12, A11, FUNCT_1:def 6; :: thesis: verum

end;

then A17: [:((proj (J,i)) .: P),((proj (J,j)) .: P):] c= <:(proj (J,i)),(proj (J,j)):> .: P by TARSKI:def 3;
<:(proj (J,i)),(proj (J,j)):> .: P c= [:((proj (J,i)) .: P),((proj (J,j)) .: P):] by FUNCT_3:56;
hence <:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):] by A17, XBOOLE_0:def 10; :: thesis: verum

end;

suppose not F is non-empty ; :: thesis: <:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):]

then {} in rng F by RELAT_1:def 9;
then P = {} by A3, CARD_3:26;
then ( <:(proj (J,i)),(proj (J,j)):> .: P = {} & (proj (J,i)) .: P = {} ) ;
hence <:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):] by ZFMISC_1:90; :: thesis: verum

end;

end;