let f be Function; :: thesis: " f is Function of bool (rng f), bool (dom f)
( dom (" f) = bool (rng f) & rng (" f) c= bool (dom f) ) by Def2, Th25;
hence " f is Function of bool (rng f), bool (dom f) by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum