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