variables_in H = (rng H) \ {0,1,2,3,4} by ZF_LANG1:def 2;
hence variables_in H is finite ; :: thesis: verum