:: deftheorem defines - MESFUNC1:def 7 :
for C being non empty set
for f being b₁ -defined ExtREAL -valued Function
for b₃ being PartFunc of C,ExtREAL holds
( b₃ = - f iff ( dom b₃ = dom f & ( for c being Element of C st c in dom b₃ holds
b₃ . c = - (f . c) ) ) );