let V be set ; :: thesis: for C being finite set
for A being Element of Fin (PFuncs (V,C)) holds Involved A c= V
let C be finite set ; :: thesis: for A being Element of Fin (PFuncs (V,C)) holds Involved A c= V
let A be Element of Fin (PFuncs (V,C)); :: thesis: Involved A c= V
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Involved A or a in V )
assume a in Involved A ; :: thesis: a in V
then consider f being finite Function such that
A1: f in A and
A2: a in dom f by Def1;
A c= PFuncs (V,C) by FINSUB_1:def 5;
then ex f1 being Function st
( f = f1 & dom f1 c= V & rng f1 c= C ) by A1, PARTFUN1:def 3;
hence a in V by A2; :: thesis: verum