let X be non empty set ; :: thesis: for S being SigmaField of X
for A being Element of S holds chi (A,X) is V75()
let S be SigmaField of X; :: thesis: for A being Element of S holds chi (A,X) is V75()
let A be Element of S; :: thesis: chi (A,X) is V75()
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

now :: thesis: |.((chi (A,X)) . x).| < +infty

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

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

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

end;

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

then (chi (A,X)) . x = 0. by FUNCT_3:def 3;
hence |.((chi (A,X)) . x).| < +infty by EXTREAL1:def 1; :: thesis: verum

end;

end;

end;

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

end;

hence chi (A,X) is V75() by Def1; :: thesis: verum