A1: firstdom F = X by Def9;

now :: thesis: ( F = {} implies rng (compose (F,X)) = {} )

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

end;

then A2: rng (compose (F,X)) c= lastrng F by Th59, 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, Th62;
hence compose (F,X) is Function of X,Y by A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum