theorem Th27: :: WAYBEL_3:27

for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I
for x being Function holds
( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )