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