let X be non empty set ; :: thesis: for S being SigmaField of X

for A being Element of S holds chi (A,X) is V82()

let S be SigmaField of X; :: thesis: for A being Element of S holds chi (A,X) is V82()

let A be Element of S; :: thesis: chi (A,X) is V82()

for x being Element of X st x in dom (chi (A,X)) holds

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

for A being Element of S holds chi (A,X) is V82()

let S be SigmaField of X; :: thesis: for A being Element of S holds chi (A,X) is V82()

let A be Element of S; :: thesis: chi (A,X) is V82()

for x being Element of X st x in dom (chi (A,X)) holds

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

proof

hence
chi (A,X) is V82()
; :: thesis: verum
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

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