theorem :: MEASUR11:62

for X being non empty set
for A being set
for er being ExtReal
for f being Function of X,ExtREAL st ( for x being Element of X holds f . x = er * ((chi (A,X)) . x) ) holds
( ( er = +infty implies f = Xchi (A,X) ) & ( er = -infty implies f = - (Xchi (A,X)) ) & ( er <> +infty & er <> -infty implies ex r being Real st
( r = er & f = r (#) (chi (A,X)) ) ) )