Union f = union (rng f) by CARD_3:def 4;
hence not Union f is empty ; :: thesis: verum