let M be MSUnTrans of f,A,B; :: thesis: M is Function-yielding

per cases ( I2 <> {} or I2 = {} ) ;

suppose I2 <> {} ; :: thesis: M is Function-yielding

then ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & M is ManySortedFunction of A,B9 * f9 ) by Def3;
hence M is Function-yielding ; :: thesis: verum

end;

suppose I2 = {} ; :: thesis: M is Function-yielding

then M = EmptyMS I1 by Def3;
hence M is Function-yielding ; :: thesis: verum

end;

end;