A1: G is finite ;
deffunc H₁( Element of bool T) -> Element of bool S = f .: T;
{ H₁(A) where A is Element of bool T : A in G } is finite from FRAENKEL:sch 21(A1);
hence f .: G is finite by Thm07; :: thesis: verum