deffunc H₁( set ) -> set = $1;
defpred S₁[ set ] means verum;
defpred S₂[ Element of PFuncs (Involved A),C] means for h being Element of PFuncs V,C st h in A holds
not $1 tolerates h;
set M = { f where f is Element of PFuncs (Involved A),C : for g being Element of PFuncs V,C st g in A holds
not f tolerates g } ;
A1: { f where f is Element of PFuncs (Involved A),C : verum } c= PFuncs (Involved A),C

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { f where f is Element of PFuncs (Involved A),C : verum } or a in PFuncs (Involved A),C )
assume a in { f where f is Element of PFuncs (Involved A),C : verum } ; :: thesis: a in PFuncs (Involved A),C
then ex f1 being Element of PFuncs (Involved A),C st f1 = a ;
hence a in PFuncs (Involved A),C ; :: thesis: verum

end;

A2: for v being Element of PFuncs (Involved A),C st S₂[v] holds
S₁[v] ;
A3: { H₁(f) where f is Element of PFuncs (Involved A),C : S₂[f] } c= { H₁(f) where f is Element of PFuncs (Involved A),C : S₁[f] } from FRAENKEL:sch 1(A2);
A4: { f where f is Element of PFuncs (Involved A),C : for g being Element of PFuncs V,C st g in A holds
not f tolerates g } c= PFuncs V,C

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { f where f is Element of PFuncs (Involved A),C : for g being Element of PFuncs V,C st g in A holds
not f tolerates g } or a in PFuncs V,C )
assume a in { f where f is Element of PFuncs (Involved A),C : for g being Element of PFuncs V,C st g in A holds
not f tolerates g } ; :: thesis: a in PFuncs V,C
then ex f1 being Element of PFuncs (Involved A),C st
( f1 = a & ( for g being Element of PFuncs V,C st g in A holds
not f1 tolerates g ) ) ;
then A5: a in PFuncs (Involved A),C ;
Involved A c= V by Th10;
then PFuncs (Involved A),C c= PFuncs V,C by PARTFUN1:128;
hence a in PFuncs V,C by A5; :: thesis: verum

end;

Involved A is finite by Th12;
then PFuncs (Involved A),C is finite by PRE_POLY:17;
hence { f where f is Element of PFuncs (Involved A),C : for g being Element of PFuncs V,C st g in A holds
not f tolerates g } is Element of Fin (PFuncs V,C) by A3, A1, A4, FINSUB_1:def 5; :: thesis: verum