let X be non empty set ; 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; 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; ( 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
; 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 verum
let c be
Complex;
for B being Element of S st f is B -measurable holds
c (#) f is B -measurable let B be
Element of
S;
( 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
;
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;
verum
end;