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