let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for c being Complex st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX
for c being Complex st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let f be PartFunc of X,COMPLEX; :: thesis: for c being Complex st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let c be Complex; :: thesis: ( f is_simple_func_in S implies c (#) f is_simple_func_in S )
assume A1: f is_simple_func_in S ; :: thesis: c (#) f is_simple_func_in S
then A2: Re f is_simple_func_in S by MESFUN7C:43;
then A3: (Im c) (#) (Re f) is_simple_func_in S by MESFUNC6:73;
A4: Im f is_simple_func_in S by A1, MESFUN7C:43;
then (Im c) (#) (Im f) is_simple_func_in S by MESFUNC6:73;
then (- 1) (#) ((Im c) (#) (Im f)) is_simple_func_in S by MESFUNC6:73;
then A5: R_EAL (- ((Im c) (#) (Im f))) is_simple_func_in S by MESFUNC6:49;
(Re c) (#) (Re f) is_simple_func_in S by A2, MESFUNC6:73;
then R_EAL ((Re c) (#) (Re f)) is_simple_func_in S by MESFUNC6:49;
then (R_EAL ((Re c) (#) (Re f))) + (R_EAL (- ((Im c) (#) (Im f)))) is_simple_func_in S by A5, MESFUNC5:38;
then R_EAL (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) is_simple_func_in S by MESFUNC6:23;
then ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) is_simple_func_in S by MESFUNC6:49;
then A6: Re (c (#) f) is_simple_func_in S by MESFUN6C:3;
(Re c) (#) (Im f) is_simple_func_in S by A4, MESFUNC6:73;
then ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) is_simple_func_in S by A3, MESFUNC6:72;
then Im (c (#) f) is_simple_func_in S by MESFUN6C:3;
hence c (#) f is_simple_func_in S by A6, MESFUN7C:43; :: thesis: verum