A1: dom (constF 0) = NAT by FUNCT_2:def 1;
rng (constF 0) c= PrimRec by Th48;
hence not PrimRec is finite by A1, CARD_1:59; :: thesis: verum