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

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

for c being Complex

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,COMPLEX st ex A being Element of S st dom f = A holds

for c being Complex

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

c (#) f is B -measurable

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

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 Complex

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 ;

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

for c being Complex

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,COMPLEX st ex A being Element of S st dom f = A holds

for c being Complex

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

c (#) f is B -measurable

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

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 Complex

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 ;

hereby :: thesis: verum

let c be Complex; :: 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 )

A2: dom ((Re c) (#) (Re f)) = dom (Re f) by VALUED_1:def 5;

A3: dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5;

dom (Re (c (#) f)) = dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) by Th3;

then A4: dom (Re (c (#) f)) = (dom ((Re c) (#) (Re f))) /\ (dom ((Im c) (#) (Im f))) by VALUED_1:12;

A5: dom ((Im c) (#) (Re f)) = dom (Re f) by VALUED_1:def 5;

dom (Im (c (#) f)) = dom (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) by Th3;

then A6: dom (Im (c (#) f)) = (dom ((Im c) (#) (Re f))) /\ (dom ((Re c) (#) (Im f))) by VALUED_1:def 1;

A7: dom ((Re c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5;

A8: dom (Re f) = dom f by COMSEQ_3:def 3;

A9: dom (Im f) = dom f by COMSEQ_3:def 4;

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

then Im f is B -measurable ;

then A11: Im f is A /\ B -measurable by A1, A9, MESFUNC6:80;

Re f is B -measurable by A10;

then Re f is A /\ B -measurable by A1, A8, MESFUNC6:80;

then f is A /\ B -measurable by A11;

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

then Im (c (#) f) is A /\ B -measurable ;

then A13: Im (c (#) f) is B -measurable by A1, A8, A9, A5, A7, A6, MESFUNC6:80;

Re (c (#) f) is A /\ B -measurable by A12;

then Re (c (#) f) is B -measurable by A1, A8, A9, A2, A3, A4, MESFUNC6:80;

hence c (#) f is B -measurable by A13; :: thesis: verum

end;c (#) f is B -measurable

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

A2: dom ((Re c) (#) (Re f)) = dom (Re f) by VALUED_1:def 5;

A3: dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5;

dom (Re (c (#) f)) = dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) by Th3;

then A4: dom (Re (c (#) f)) = (dom ((Re c) (#) (Re f))) /\ (dom ((Im c) (#) (Im f))) by VALUED_1:12;

A5: dom ((Im c) (#) (Re f)) = dom (Re f) by VALUED_1:def 5;

dom (Im (c (#) f)) = dom (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) by Th3;

then A6: dom (Im (c (#) f)) = (dom ((Im c) (#) (Re f))) /\ (dom ((Re c) (#) (Im f))) by VALUED_1:def 1;

A7: dom ((Re c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5;

A8: dom (Re f) = dom f by COMSEQ_3:def 3;

A9: dom (Im f) = dom f by COMSEQ_3:def 4;

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

then Im f is B -measurable ;

then A11: Im f is A /\ B -measurable by A1, A9, MESFUNC6:80;

Re f is B -measurable by A10;

then Re f is A /\ B -measurable by A1, A8, MESFUNC6:80;

then f is A /\ B -measurable by A11;

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

then Im (c (#) f) is A /\ B -measurable ;

then A13: Im (c (#) f) is B -measurable by A1, A8, A9, A5, A7, A6, MESFUNC6:80;

Re (c (#) f) is A /\ B -measurable by A12;

then Re (c (#) f) is B -measurable by A1, A8, A9, A2, A3, A4, MESFUNC6:80;

hence c (#) f is B -measurable by A13; :: thesis: verum