# Re: [tlaplus] Function domains in TLAPS

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