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