:: deftheorem Def4 defines - SUPINF_2:def 4 :
for X being non empty set
for Y being non empty Subset of ExtREAL
for F being Function of X,Y
for b₄ being Function of X,(- Y) holds
( b₄ = - F iff for x being Element of X holds b₄ . x = - (F . x) );