You seem to think that for any function f, you should be able to deduce
(f[3] = 8) => (3 \in DOMAIN f)
That formula is equivalent to
(3 \notin DOMAIN f) => (f[3] # 8)
From what general properties of functions would you expect to be able
to deduce this?
Leslie