let A, B be set ; :: thesis: for R being Subset of [:A,B:] holds .: is Function of (bool A),(bool (rng R))
let R be Subset of [:A,B:]; :: thesis: .: is Function of (bool A),(bool (rng R))
( dom (.: ) = bool A & rng (.: ) c= bool (rng R) ) by Def3, Th20;
hence .: is Function of (bool A),(bool (rng R)) by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum