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