:: deftheorem Def3 defines MSUnTrans FUNCTOR0:def 3 :
for I1, I2 being 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
( ( I2 <> {} implies ( b₆ is MSUnTrans of f,A,B iff ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & b₆ is ManySortedFunction of A,B9 * f9 ) ) ) & ( not I2 <> {} implies ( b₆ is MSUnTrans of f,A,B iff b₆ = EmptyMS I1 ) ) );