let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,REAL 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 f being PartFunc of X,REAL 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,REAL; :: 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, Th80;
then A2: c (#) f is A /\ B -measurable by A1, Th21, XBOOLE_1:17;
dom (c (#) f) = A by A1, VALUED_1:def 5;
hence c (#) f is B -measurable by A2, Th80; :: thesis: verum