A1: dom (.: ) = bool A by Def3;
.: is Function of bool A, bool (rng R) by Th21;
then A2: rng (.: ) c= bool (rng R) by RELAT_1:def 19;
bool (rng R) c= bool B by ZFMISC_1:79;
then rng (.: ) c= bool B by A2, XBOOLE_1:1;
hence .: R,A is Function of bool A, bool B by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum