let M be ManySortedSet of ; :: 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 I2' being non empty set ex B' being ManySortedSet of ex f' being Function of I1,I2' st
( f = f' & B = B' & M is ManySortedFunction of A,B' * f' ) by Def4;
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 Def4; :: thesis: verum