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