let V, C be set ; PFuncs (V,C) c= bool [:V,C:]
let x be object ; TARSKI:def 3 ( not x in PFuncs (V,C) or x in bool [:V,C:] )
assume
x in PFuncs (V,C)
; 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 3;
A4:
f c= [:(dom f),(rng f):]
by RELAT_1:7;
[:(dom f),(rng f):] c= [:V,C:]
by A2, A3, ZFMISC_1:96;
then
f c= [:V,C:]
by A4;
hence
x in bool [:V,C:]
by A1; verum