A2: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def4;
( dom f1 = X & dom f2 = X ) by PARTFUN1:def 2;
hence f1 (#) f2 is total by A2, PARTFUN1:def 2; :: thesis: verum