( f = f & dom f = X & rng f c= Y ) by PARTFUN1:def 2;
then f in Funcs (X,Y) by FUNCT_2:def 2;
hence {f} \ (Funcs (X,Y)) is empty by Th29; :: thesis: verum