ex f being Function st
( dom f c= X & rng f c= Y ) by Lm2;
hence not PFuncs X,Y is empty by Def5; :: thesis: verum