let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for c being complex number 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 number 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 number st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let c be complex number ; :: thesis: ( f is_simple_func_in S implies c (#) f is_simple_func_in S )
assume f is_simple_func_in S ; :: thesis: c (#) f is_simple_func_in S
then ( Re f is_simple_func_in S & Im f is_simple_func_in S ) by MESFUN7C:43;
then A1: ( (Re c) (#) (Re f) is_simple_func_in S & (Re c) (#) (Im f) is_simple_func_in S & (Im c) (#) (Re f) is_simple_func_in S & (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 A4: R_EAL (- ((Im c) (#) (Im f))) is_simple_func_in S by MESFUNC6:49;
R_EAL ((Re c) (#) (Re f)) is_simple_func_in S by A1, MESFUNC6:49;
then A5: (R_EAL ((Re c) (#) (Re f))) + (R_EAL (- ((Im c) (#) (Im f)))) is_simple_func_in S by A4, MESFUNC5:44;
R_EAL (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) is_simple_func_in S by A5, MESFUNC6:23;
then A6: ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) is_simple_func_in S by MESFUNC6:49;
((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) is_simple_func_in S by A1, MESFUNC6:72;
then ( Re (c (#) f) is_simple_func_in S & Im (c (#) f) is_simple_func_in S ) by A6, MESFUN6C:3;
hence c (#) f is_simple_func_in S by MESFUN7C:43; :: thesis: verum