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