let V, C be non empty set ; :: thesis: ex f being Element of PFuncs V,C st f <> {}
consider a being set such that
A1: a in V by XBOOLE_0:def 1;
consider b being set such that
A2: b in C by XBOOLE_0:def 1;
set f = {[a,b]};
( {a} c= V & {b} c= C ) by A1, A2, ZFMISC_1:37;
then ( dom {[a,b]} c= V & rng {[a,b]} c= C ) by RELAT_1:23;
then reconsider f = {[a,b]} as Element of PFuncs V,C by PARTFUN1:def 5;
f <> {} ;
hence ex f being Element of PFuncs V,C st f <> {} ; :: thesis: verum