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 Th22, RELAT_1:111;
hence (" f) .: B c= bool (dom f) ; :: thesis: verum