deffunc H₁( Element of V) -> Element of the carrier of V = v + V;
card { H₁(w) where w is Element of V : w in A } c= card A from TREES_2:sch 2();
then card (v + A) is finite by RUSUB_4:def 8;
hence v + A is finite ; :: thesis: verum