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

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st ex A being Element of S st dom f = A holds

for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st ex A being Element of S st dom f = A holds

for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st dom f = A holds

for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

let f be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st dom f = A implies for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable )

assume ex A being Element of S st A = dom f ; :: thesis: for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

then consider A being Element of S such that

A1: A = dom f ;

let c be Real; :: thesis: for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

let B be Element of S; :: thesis: ( f is B -measurable implies c (#) f is B -measurable )

assume f is B -measurable ; :: thesis: c (#) f is B -measurable

then f is A /\ B -measurable by A1, Th48;

then A2: c (#) f is A /\ B -measurable by A1, MESFUNC1:37, XBOOLE_1:17;

dom (c (#) f) = A by A1, MESFUNC1:def 6;

hence c (#) f is B -measurable by A2, Th48; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st ex A being Element of S st dom f = A holds

for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st ex A being Element of S st dom f = A holds

for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st dom f = A holds

for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

let f be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st dom f = A implies for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable )

assume ex A being Element of S st A = dom f ; :: thesis: for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

then consider A being Element of S such that

A1: A = dom f ;

let c be Real; :: thesis: for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

let B be Element of S; :: thesis: ( f is B -measurable implies c (#) f is B -measurable )

assume f is B -measurable ; :: thesis: c (#) f is B -measurable

then f is A /\ B -measurable by A1, Th48;

then A2: c (#) f is A /\ B -measurable by A1, MESFUNC1:37, XBOOLE_1:17;

dom (c (#) f) = A by A1, MESFUNC1:def 6;

hence c (#) f is B -measurable by A2, Th48; :: thesis: verum