( dom (f +* (i,x)) = dom f & dom f = I ) by FUNCT_7:30, PARTFUN1:def 2;
hence f +* (i,x) is ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18; :: thesis: verum