let A be set ; :: thesis: for f being Function holds (" f) " A c= bool (rng f)
let f be Function; :: thesis: (" f) " A c= bool (rng f)
dom (" f) = bool (rng f) by Def2;
hence (" f) " A c= bool (rng f) by RELAT_1:132; :: thesis: verum