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