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 A1: ( Y = {} implies X = {} ) ; :: thesis: .: f is Function of (bool X),(bool Y)
A2: .: f is Function of (bool (dom f)),(bool (rng f)) by Th21;
A3: ( dom f = X & rng f c= Y ) by A1, FUNCT_2:def 1, RELAT_1:def 19;
A4: ( dom (.: f) = bool (dom f) & rng (.: f) c= bool (rng f) ) by A2, FUNCT_2:def 1, RELAT_1:def 19;
rng f c= Y by RELAT_1:def 19;
then bool (rng f) c= bool Y by ZFMISC_1:79;
then rng (.: f) c= bool Y by A4, XBOOLE_1:1;
hence .: f is Function of (bool X),(bool Y) by A3, A4, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum