let B be set ; :: thesis: for f being Function holds (" f) .: B c= bool (dom f)
let f be Function; :: thesis: (" f) .: B c= bool (dom f)
( rng (" f) c= bool (dom f) & (" f) .: B c= rng (" f) ) by Th25, RELAT_1:144;
hence (" f) .: B c= bool (dom f) by XBOOLE_1:1; :: thesis: verum