A1: G is countable ;
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 countable from SRINGS_4:sch 1(A1);
hence f .: G is countable by Thm07; :: thesis: verum