let g be Function; :: thesis: {} .. g = {}
dom ({} .. g) = (dom {}) /\ (dom g) by PRALG_1:def 19
.= dom {} ;
hence {} .. g = {} ; :: thesis: verum