A1: ( firstdom F = X & lastrng F c= Y ) by Def9;

now

assume F = {} ; :: thesis: rng (compose F,X) = {}
then ( X = {} & compose F,X = id X ) by A1, Def6, Th41;
hence rng (compose F,X) = {} ; :: thesis: verum

end;

then rng (compose F,X) c= lastrng F by Th61, XBOOLE_1:2;
then ( dom (compose F,X) = X & rng (compose F,X) c= Y ) by A1, Th64, XBOOLE_1:1;
hence compose F,X is Function of X,Y by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum