for I being non empty set
for J1, J2 being non-Empty TopSpace-yielding ManySortedSet of I st ( for i being Element of I holds J1 . i is SubSpace of J2 . i ) holds
product J1 is SubSpace of product J2