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