let X be non empty set ; :: thesis:
let A be set ; :: thesis:
let er be ExtReal; :: thesis:
let f be Function of X,ExtREAL; :: thesis:
assume A1: for x being Element of X holds f . x = er * ((chi (A,X)) . x) ; :: thesis:

hereby :: thesis:

assume A2: er = +infty ; :: thesis:
for x being Element of X holds f . x = (Xchi (A,X)) . x

proof

let x be Element of X; :: thesis:

per cases ;

suppose A3: x in A ; :: thesis:

then A4: (Xchi (A,X)) . x = +infty by MEASUR10:def 7;
(chi (A,X)) . x = 1 by A3, FUNCT_3:def 3;
then f . x = er * 1 by A1;
hence f . x = (Xchi (A,X)) . x by A2, A4, XXREAL_3:81; :: thesis:

end;

suppose A5: not x in A ; :: thesis:

then (chi (A,X)) . x = 0 by FUNCT_3:def 3;
then f . x = er * 0 by A1;
hence f . x = (Xchi (A,X)) . x by A5, MEASUR10:def 7; :: thesis:

end;

end;

end;

hence f = Xchi (A,X) by FUNCT_2:def 8; :: thesis:

end;

hereby :: thesis:

assume A6: er = -infty ; :: thesis:
for x being Element of X holds f . x = (- (Xchi (A,X))) . x

proof

let x be Element of X; :: thesis:
dom (Xchi (A,X)) = X by FUNCT_2:def 1;
then x in dom (Xchi (A,X)) ;
then A7: x in dom (- (Xchi (A,X))) by MESFUNC1:def 7;

per cases ;

suppose A8: x in A ; :: thesis:

then (Xchi (A,X)) . x = +infty by MEASUR10:def 7;
then A9: (- (Xchi (A,X))) . x = - +infty by A7, MESFUNC1:def 7;
(chi (A,X)) . x = 1 by A8, FUNCT_3:def 3;
then f . x = er * 1 by A1;
hence f . x = (- (Xchi (A,X))) . x by A6, A9, XXREAL_3:6, XXREAL_3:81; :: thesis:

end;

suppose A10: not x in A ; :: thesis:

then A11: - ((Xchi (A,X)) . x) = - 0 by MEASUR10:def 7;
(chi (A,X)) . x = 0 by A10, FUNCT_3:def 3;
then f . x = er * 0 by A1;
hence f . x = (- (Xchi (A,X))) . x by A7, A11, MESFUNC1:def 7; :: thesis:

end;

end;

end;

hence f = - (Xchi (A,X)) by FUNCT_2:def 8; :: thesis:

end;

assume ( er <> +infty & er <> -infty ) ; :: thesis:
then er in REAL by XXREAL_0:14;
then reconsider r = er as Real ;
( dom f = X & dom (chi (A,X)) = X ) by FUNCT_2:def 1;
then A12: dom f = dom (r (#) (chi (A,X))) by MESFUNC1:def 6;
for x being Element of X st x in dom f holds
f . x = (r (#) (chi (A,X))) . x

proof

let x be Element of X; :: thesis:
assume x in dom f ; :: thesis:
then (r (#) (chi (A,X))) . x = r * ((chi (A,X)) . x) by A12, MESFUNC1:def 6;
hence f . x = (r (#) (chi (A,X))) . x by A1; :: thesis:

end;

hence ex r being Real st
( r = er & f = r (#) (chi (A,X)) ) by A12, PARTFUN1:5; :: thesis: