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))
A1: dom (.: ) = bool A by Def1;
rng (.: ) c= bool (rng R) by Th20;
hence .: is Function of (bool A),(bool (rng R)) by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum