A1: firstdom F = X 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 A2: rng (compose F,X) c= lastrng F by Th61, XBOOLE_1:2;
lastrng F c= Y by Def9;
then A3: rng (compose F,X) c= Y by A2, XBOOLE_1:1;
dom (compose F,X) = X by A1, Th64;
hence compose F,X is Function of X,Y by A3, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum