let X be non empty set ; :: thesis: for S being SigmaField of X
for A being Element of S holds chi A,X is real-valued
let S be SigmaField of X; :: thesis: for A being Element of S holds chi A,X is real-valued
let A be Element of S; :: thesis: chi A,X is real-valued
A1: for x being Element of X st x in dom (chi A,X) holds
|.((chi A,X) . x).| < +infty

proof

let x be Element of X; :: thesis: ( x in dom (chi A,X) implies |.((chi A,X) . x).| < +infty )
assume x in dom (chi A,X) ; :: thesis: |.((chi A,X) . x).| < +infty

A2: now

per cases ( x in A or not x in A ) ;

suppose A3: x in A ; :: thesis: |.((chi A,X) . x).| < +infty

A4: (chi A,X) . x = 1. by A3, FUNCT_3:def 3, MESFUNC1:def 8;
A5: |.((chi A,X) . x).| = 1. by A4, EXTREAL1:def 3, MESFUNC1:def 8;
thus |.((chi A,X) . x).| < +infty by A5, MESFUNC1:def 8, XXREAL_0:9; :: thesis: verum

end;

suppose A6: not x in A ; :: thesis: |.((chi A,X) . x).| < +infty

A7: (chi A,X) . x = 0. by A6, FUNCT_3:def 3;
thus |.((chi A,X) . x).| < +infty by A7, EXTREAL1:def 3; :: thesis: verum

end;

end;

end;

thus |.((chi A,X) . x).| < +infty by A2; :: thesis: verum

end;

thus chi A,X is real-valued by A1, Def1; :: thesis: verum