A1: ( dom f = I1 & dom g = I1 ) by PARTFUN1:def 4;
dom (g ** f) = (dom g) /\ (dom f) by PBOOLE:def 24
.= I1 by A1 ;
hence g ** f is ManySortedFunction of by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum