:: deftheorem Def3 defines - NFCONT_4:def 3 :
for n being Element of NAT
for Z being non empty set
for f, b₄ being PartFunc of Z,(REAL n) holds
( b₄ = - f iff ( dom b₄ = dom f & ( for c being set st c in dom b₄ holds
b₄ /. c = - (f /. c) ) ) );