deffunc H₁( Element of CQC-WFF Al) -> Element of bool (bound_QC-variables Al) = still_not-bound_in Al;
A1: for x being set st x in { H₁(p) where p is Element of CQC-WFF Al : p in PHI } holds
x is finite

proof

let x be set ; :: thesis: ( x in { H₁(p) where p is Element of CQC-WFF Al : p in PHI } implies x is finite )
assume A2: x in { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in PHI } ; :: thesis: x is finite
ex p being Element of CQC-WFF Al st
( x = still_not-bound_in p & p in PHI ) by A2;
hence x is finite by CQC_SIM1:19; :: thesis: verum

end;

A3: PHI is finite ;
{ H₁(p) where p is Element of CQC-WFF Al : p in PHI } is finite from FRAENKEL:sch 21(A3);
then union { H₁(p) where p is Element of CQC-WFF Al : p in PHI } is finite by A1, FINSET_1:7;
hence still_not-bound_in PHI is finite by GOEDELCP:def 8; :: thesis: verum