let X, Y be set ; :: thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds
.: f is Function of (bool X),(bool Y)
let f be Function of X,Y; :: thesis: ( ( Y = {} implies X = {} ) implies .: f is Function of (bool X),(bool Y) )
assume ( Y = {} implies X = {} ) ; :: thesis: .: f is Function of (bool X),(bool Y)
then A1: dom f = X by FUNCT_2:def 1;
rng f c= Y by RELAT_1:def 19;
then A2: bool (rng f) c= bool Y by ZFMISC_1:67;
A3: .: f is Function of (bool (dom f)),(bool (rng f)) by Th19;
then rng (.: f) c= bool (rng f) by RELAT_1:def 19;
then A4: rng (.: f) c= bool Y by A2;
dom (.: f) = bool (dom f) by A3, FUNCT_2:def 1;
hence .: f is Function of (bool X),(bool Y) by A1, A4, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum