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