let f be Function; :: thesis: (.: f) . {} = {}
{} c= dom f by XBOOLE_1:2;
then (.: f) . {} = f .: {} by Def1;
hence (.: f) . {} = {} by RELAT_1:149; :: thesis: verum