let M be ManySortedSet of I1; :: thesis: ( M is MSUnTrans of f,A,B iff M is ManySortedFunction of A,B * f )

hereby :: thesis: ( M is ManySortedFunction of A,B * f implies M is MSUnTrans of f,A,B )

assume M is MSUnTrans of f,A,B ; :: thesis: M is ManySortedFunction of A,B * f
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 ManySortedFunction of A,B * f ; :: thesis: verum

end;

thus ( M is ManySortedFunction of A,B * f implies M is MSUnTrans of f,A,B ) by Def3; :: thesis: verum