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