let f be Function; :: thesis: .: f is Function of (bool (dom f)),(bool (rng f))
( dom (.: f) = bool (dom f) & rng (.: f) c= bool (rng f) ) by Def1, Th9;
hence .: f is Function of (bool (dom f)),(bool (rng f)) by FUNCT_2:def 1, RELSET_1:4; :: thesis: verum