theorem Th72: :: TOPS_5:72

for I being non empty set
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):]