rng f c= (rng (f | (support f))) \/ {0} by Th2;
hence rng f is finite ; :: thesis: verum