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 and
A3: rng f c= C by PARTFUN1:def 5;
A4: f c= [:(dom f),(rng f):] by RELAT_1:21;
[:(dom f),(rng f):] c= [:V,C:] by A2, A3, ZFMISC_1:119;
then f c= [:V,C:] by A4, XBOOLE_1:1;
hence x in bool [:V,C:] by A1; :: thesis: verum