theorem Th73: :: TOPS_5:73

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds
( f is onto & f is open )