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

for A, B being Element of S holds chi (A,X) is B -measurable

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

let A, B be Element of S; :: thesis: chi (A,X) is B -measurable

for r being Real holds B /\ (less_eq_dom ((chi (A,X)),r)) in S

for A, B being Element of S holds chi (A,X) is B -measurable

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

let A, B be Element of S; :: thesis: chi (A,X) is B -measurable

for r being Real holds B /\ (less_eq_dom ((chi (A,X)),r)) in S

proof

hence
chi (A,X) is B -measurable
by MESFUNC1:28; :: thesis: verum
let r be Real; :: thesis: B /\ (less_eq_dom ((chi (A,X)),r)) in S

reconsider r = r as Real ;

end;reconsider r = r as Real ;

now :: thesis: B /\ (less_eq_dom ((chi (A,X)),r)) in Send;

hence
B /\ (less_eq_dom ((chi (A,X)),r)) in S
; :: thesis: verumper cases
( r >= 1 or ( 0 <= r & r < 1 ) or r < 0 )
;

end;

suppose A1:
r >= 1
; :: thesis: B /\ (less_eq_dom ((chi (A,X)),r)) in S

for x being object st x in X holds

x in less_eq_dom ((chi (A,X)),r)

then less_eq_dom ((chi (A,X)),r) = X ;

then less_eq_dom ((chi (A,X)),r) in S by PROB_1:5;

hence B /\ (less_eq_dom ((chi (A,X)),r)) in S by FINSUB_1:def 2; :: thesis: verum

end;x in less_eq_dom ((chi (A,X)),r)

proof

then
X c= less_eq_dom ((chi (A,X)),r)
;
let x be object ; :: thesis: ( x in X implies x in less_eq_dom ((chi (A,X)),r) )

assume A2: x in X ; :: thesis: x in less_eq_dom ((chi (A,X)),r)

then A3: x in dom (chi (A,X)) by FUNCT_3:def 3;

reconsider x = x as Element of X by A2;

(chi (A,X)) . x <= 1. then (chi (A,X)) . x <= r by A1, XXREAL_0:2;

hence x in less_eq_dom ((chi (A,X)),r) by A3, MESFUNC1:def 12; :: thesis: verum

end;assume A2: x in X ; :: thesis: x in less_eq_dom ((chi (A,X)),r)

then A3: x in dom (chi (A,X)) by FUNCT_3:def 3;

reconsider x = x as Element of X by A2;

(chi (A,X)) . x <= 1. then (chi (A,X)) . x <= r by A1, XXREAL_0:2;

hence x in less_eq_dom ((chi (A,X)),r) by A3, MESFUNC1:def 12; :: thesis: verum

then less_eq_dom ((chi (A,X)),r) = X ;

then less_eq_dom ((chi (A,X)),r) in S by PROB_1:5;

hence B /\ (less_eq_dom ((chi (A,X)),r)) in S by FINSUB_1:def 2; :: thesis: verum

suppose A4:
( 0 <= r & r < 1 )
; :: thesis: B /\ (less_eq_dom ((chi (A,X)),r)) in S

for x being object st x in less_eq_dom ((chi (A,X)),r) holds

x in X \ A

for x being object st x in X \ A holds

x in less_eq_dom ((chi (A,X)),r)

then A11: less_eq_dom ((chi (A,X)),r) = X \ A by A6;

X in S by PROB_1:5;

then less_eq_dom ((chi (A,X)),r) in S by A11, MEASURE1:6;

hence B /\ (less_eq_dom ((chi (A,X)),r)) in S by FINSUB_1:def 2; :: thesis: verum

end;x in X \ A

proof

then A6:
less_eq_dom ((chi (A,X)),r) c= X \ A
;
let x be object ; :: thesis: ( x in less_eq_dom ((chi (A,X)),r) implies x in X \ A )

assume A5: x in less_eq_dom ((chi (A,X)),r) ; :: thesis: x in X \ A

then reconsider x = x as Element of X ;

(chi (A,X)) . x <= r by A5, MESFUNC1:def 12;

then not x in A by A4, FUNCT_3:def 3;

hence x in X \ A by XBOOLE_0:def 5; :: thesis: verum

end;assume A5: x in less_eq_dom ((chi (A,X)),r) ; :: thesis: x in X \ A

then reconsider x = x as Element of X ;

(chi (A,X)) . x <= r by A5, MESFUNC1:def 12;

then not x in A by A4, FUNCT_3:def 3;

hence x in X \ A by XBOOLE_0:def 5; :: thesis: verum

for x being object st x in X \ A holds

x in less_eq_dom ((chi (A,X)),r)

proof

then
X \ A c= less_eq_dom ((chi (A,X)),r)
;
let x be object ; :: thesis: ( x in X \ A implies x in less_eq_dom ((chi (A,X)),r) )

assume A7: x in X \ A ; :: thesis: x in less_eq_dom ((chi (A,X)),r)

then A8: x in X ;

A9: not x in A by A7, XBOOLE_0:def 5;

reconsider x = x as Element of X by A7;

A10: (chi (A,X)) . x = 0. by A9, FUNCT_3:def 3;

x in dom (chi (A,X)) by A8, FUNCT_3:def 3;

hence x in less_eq_dom ((chi (A,X)),r) by A4, A10, MESFUNC1:def 12; :: thesis: verum

end;assume A7: x in X \ A ; :: thesis: x in less_eq_dom ((chi (A,X)),r)

then A8: x in X ;

A9: not x in A by A7, XBOOLE_0:def 5;

reconsider x = x as Element of X by A7;

A10: (chi (A,X)) . x = 0. by A9, FUNCT_3:def 3;

x in dom (chi (A,X)) by A8, FUNCT_3:def 3;

hence x in less_eq_dom ((chi (A,X)),r) by A4, A10, MESFUNC1:def 12; :: thesis: verum

then A11: less_eq_dom ((chi (A,X)),r) = X \ A by A6;

X in S by PROB_1:5;

then less_eq_dom ((chi (A,X)),r) in S by A11, MEASURE1:6;

hence B /\ (less_eq_dom ((chi (A,X)),r)) in S by FINSUB_1:def 2; :: thesis: verum

suppose A12:
r < 0
; :: thesis: B /\ (less_eq_dom ((chi (A,X)),r)) in S

for x being Element of X holds not x in less_eq_dom ((chi (A,X)),r)

hence B /\ (less_eq_dom ((chi (A,X)),r)) in S by PROB_1:4; :: thesis: verum

end;proof

then
less_eq_dom ((chi (A,X)),r) = {}
by SUBSET_1:4;
assume
ex x being Element of X st x in less_eq_dom ((chi (A,X)),r)
; :: thesis: contradiction

then consider x being Element of X such that

A13: x in less_eq_dom ((chi (A,X)),r) ;

0. <= (chi (A,X)) . x hence contradiction by A12, A13, MESFUNC1:def 12; :: thesis: verum

end;then consider x being Element of X such that

A13: x in less_eq_dom ((chi (A,X)),r) ;

0. <= (chi (A,X)) . x hence contradiction by A12, A13, MESFUNC1:def 12; :: thesis: verum

hence B /\ (less_eq_dom ((chi (A,X)),r)) in S by PROB_1:4; :: thesis: verum