theorem Th18: :: FUNCTOR0:18

for I1, I2 being non empty set
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for o being Element of I2 st B . o <> {} holds
for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B