for X being non empty TopSpace
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being Function of X,(product J) holds
( f is continuous iff for i being Element of I holds (proj (J,i)) * f is continuous )