(dom f) +^ (dom g) <> 0 by ORDINAL3:26;
then dom (f ^ g) <> 0 by ORDINAL4:def 1;
hence not f ^ g is empty ; :: thesis: verum