let f be ManySortedFunction of A,B; :: thesis: f is Function-yielding
let i be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in dom f or f . i is set )
assume i in dom f ; :: thesis: f . i is set
then i in I by PARTFUN1:def 2;
hence f . i is set by Def15; :: thesis: verum