let f be Function of A,B; :: thesis: f is non-empty
thus not {} in rng f ; :: according to RELAT_1:def 9 :: thesis: verum