dom x = NAT by FUNCT_2:def 1;
then n c= dom x by ORDINAL1:def 2, ORDINAL1:def 12;
hence dom (x | n) = n by RELAT_1:62; :: thesis: verum