let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A, B, C being Element of S
for er being ExtReal st C c= B holds
(chi (er,A,X)) | B is_measurable_on C
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for A, B, C being Element of S
for er being ExtReal st C c= B holds
(chi (er,A,X)) | B is_measurable_on C
let M be sigma_Measure of S; :: thesis: for A, B, C being Element of S
for er being ExtReal st C c= B holds
(chi (er,A,X)) | B is_measurable_on C
let A, B, C be Element of S; :: thesis: for er being ExtReal st C c= B holds
(chi (er,A,X)) | B is_measurable_on C
let er be ExtReal; :: thesis: ( C c= B implies (chi (er,A,X)) | B is_measurable_on C )
assume a1: C c= B ; :: thesis: (chi (er,A,X)) | B is_measurable_on C
dom (chi (er,A,X)) = X by FUNCT_2:def 1;
then B = (dom (chi (er,A,X))) /\ B by XBOOLE_1:28;
then (chi (er,A,X)) | B is_measurable_on B by Th13, MESFUNC5:42;
hence (chi (er,A,X)) | B is_measurable_on C by a1, MESFUNC1:30; :: thesis: verum