theorem :: FUNCT_3:35

for f being Function holds " f is Function of (bool (rng f)),(bool (dom f))