:: deftheorem DefXchi defines Xchi MEASUR10:def 7 :
for A, X being set
for b₃ being Function of X,ExtREAL holds
( b₃ = Xchi (A,X) iff for x being object st x in X holds
( ( x in A implies b₃ . x = +infty ) & ( not x in A implies b₃ . x = 0 ) ) );