let V, C be set ; :: thesis: PFuncs V,C c= bool [:V,C:]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PFuncs V,C or x in bool [:V,C:] )
assume x in PFuncs V,C ; :: thesis: x in bool [:V,C:]
then consider f being Function such that
A1: x = f and
A2: ( dom f c= V & rng f c= C ) by PARTFUN1:def 5;
A3: f c= [:(dom f),(rng f):] by RELAT_1:21;
[:(dom f),(rng f):] c= [:V,C:] by A2, ZFMISC_1:119;
then f c= [:V,C:] by A3, XBOOLE_1:1;
hence x in bool [:V,C:] by A1; :: thesis: verum