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 set ; :: 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 & a in dom f ) by Def1;
A c= PFuncs V,C by FINSUB_1:def 5;
then consider f1 being Function such that
A2: ( f = f1 & dom f1 c= V & rng f1 c= C ) by A1, PARTFUN1:def 5;
thus a in V by A1, A2; :: thesis: verum