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 } ;
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;
defpred S₂[ set ] means verum;
A1: for v being Element of PFuncs (Involved A),C st S₁[v] holds
S₂[v] ;
deffunc H₁( set ) -> set = $1;
A2: { 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(A1);
Involved A is finite by Th12;
then A3: PFuncs (Involved A),C is finite by Th5;
{ 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 consider f1 being Element of PFuncs (Involved A),C such that
A4: f1 = a ;
thus a in PFuncs (Involved A),C by A4; :: thesis: verum

end;

then A5: { 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 finite by A2, A3;
{ 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 consider f1 being Element of PFuncs (Involved A),C such that
A6: ( f1 = a & ( for g being Element of PFuncs V,C st g in A holds
not f1 tolerates g ) ) ;
Involved A c= V by Th10;
then A7: PFuncs (Involved A),C c= PFuncs V,C by PARTFUN1:128;
a in PFuncs (Involved A),C by A6;
hence a in PFuncs V,C by A7; :: thesis: verum

end;

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 A5, FINSUB_1:def 5; :: thesis: verum