A1: ( dom f = I1 & dom g = I1 ) by PARTFUN1:def 2;
dom (g ** f) = (dom g) /\ (dom f) by PBOOLE:def 19
.= I1 by A1 ;
hence g ** f is I1 -defined ; :: thesis: verum