:: deftheorem Def4 defines MSUnTrans FUNCTOR0:def 4 :
for I1 being set
for I2 being non empty set
for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for b₆ being ManySortedSet of I1 holds
( b₆ is MSUnTrans of f,A,B iff b₆ is ManySortedFunction of A,B * f );