A1: firstdom F = X by Def8;

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

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

end;

then A2: rng (compose (F,X)) c= lastrng F by Th58;
lastrng F c= Y by Def8;
then A3: rng (compose (F,X)) c= Y by A2;
dom (compose (F,X)) = X by A1, Th61;
hence compose (F,X) is Function of X,Y by A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum