theorem Th31: :: WAYBEL_5:31

for J, A being non empty set
for B being set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,A
for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B