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