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;