let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being Subset of (product ())
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= () . 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 ())
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= () . k ) ) holds
<:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):]

let P be Subset of (product ()); :: 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= () . 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= () . 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= () . 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= () . 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 () 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= () . k by A4;
then ( (proj ((),i)) .: P = F . i & (proj ((),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 ((),i))) /\ (dom (proj (J,j))) by WAYBEL18:def 4
.= (dom (proj ((),i))) /\ (dom (proj ((),j))) by WAYBEL18:def 4 ;
then A11: dom <:(proj (J,i)),(proj (J,j)):> = (dom (proj ((),i))) /\ (product ()) by CARD_3:def 16
.= (product ()) /\ (product ()) by CARD_3:def 16
.= product () ;
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 ((),i)) & the Element of product F +* ((i,j) --> (y1,y2)) in dom (proj ((),j)) ) by ;
A15: (proj (J,i)) . ( the Element of product F +* ((i,j) --> (y1,y2))) = (proj ((),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
.= y1 by ;
A16: (proj (J,j)) . ( the Element of product F +* ((i,j) --> (y1,y2))) = (proj ((),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
.= y2 by ;
<:(proj (J,i)),(proj (J,j)):> . ( the Element of product F +* ((i,j) --> (y1,y2))) = [y1,y2] by ;
hence y in <:(proj (J,i)),(proj (J,j)):> .: P by ; :: 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 ; :: 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 ;
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;