let a be Data-Location ; :: thesis: for f being NAT -defined Function holds not a in dom f
let f be NAT -defined Function; :: thesis: not a in dom f
dom f c= NAT by RELAT_1:def 18;
hence not a in dom f by Th74; :: thesis: verum