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)
( (.: f) .: A c= rng (.: f) & rng (.: f) c= bool (rng f) ) by Th10, RELAT_1:111;
hence (.: f) .: A c= bool (rng f) by XBOOLE_1:1; :: thesis: verum