let g be Function; :: thesis: {} .. g = {}
dom {} = {} ;
then dom ({} .. g) = {} by PRALG_1:def 17;
hence {} .. g = {} ; :: thesis: verum