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:79;
A3: .: f is Function of bool (dom f), bool (rng f) by Th21;
then rng (.: f) c= bool (rng f) by RELAT_1:def 19;
then A4: rng (.: f) c= bool Y by A2, XBOOLE_1:1;
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:11; :: thesis: verum