let X be non empty set ; :: thesis: for f being PartFunc of X,COMPLEX
for c being complex number holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
let f be PartFunc of X,COMPLEX ; :: thesis: for c being complex number holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
let c be complex number ; :: thesis: ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
A0: ( dom (Re (c (#) f)) = dom (c (#) f) & dom (Re f) = dom f & dom (Im (c (#) f)) = dom (c (#) f) & dom (Im f) = dom f ) by Def1, Def2;
A1: ( dom ((Re c) (#) (Re f)) = dom (Re f) & dom ((Im c) (#) (Im f)) = dom (Im f) & dom ((Im c) (#) (Re f)) = dom (Re f) & dom ((Re c) (#) (Im f)) = dom (Im f) & dom (c (#) f) = dom f ) by VALUED_1:def 5;
A2: dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) = (dom ((Re c) (#) (Re f))) /\ (dom ((Im c) (#) (Im f))) by VALUED_1:12;

now

let x be set ; :: thesis: ( x in dom (Re (c (#) f)) implies (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x )
assume P01: x in dom (Re (c (#) f)) ; :: thesis: (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x
then (Re (c (#) f)) . x = Re ((c (#) f) . x) by Def1;
then Q01: (Re (c (#) f)) . x = Re (c * (f . x)) by P01, A0, VALUED_1:def 5;
P05: ( ((Re c) (#) (Re f)) . x = (Re c) * ((Re f) . x) & ((Im c) (#) (Im f)) . x = (Im c) * ((Im f) . x) & (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by P01, A0, A1, Def1, Def2, VALUED_1:def 5;
Re (c * (f . x)) = ((Re c) * (Re (f . x))) - ((Im c) * (Im (f . x))) by COMPLEX1:24;
hence (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x by Q01, P01, P05, A0, A2, A1, VALUED_1:13; :: thesis: verum

end;

hence Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) by A0, A2, A1, FUNCT_1:9; :: thesis: Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f))
B2: dom (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) = (dom ((Im c) (#) (Re f))) /\ (dom ((Re c) (#) (Im f))) by VALUED_1:def 1;

now

let x be set ; :: thesis: ( x in dom (Im (c (#) f)) implies (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x )
assume P01: x in dom (Im (c (#) f)) ; :: thesis: (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x
then (Im (c (#) f)) . x = Im ((c (#) f) . x) by Def2;
then Q01: (Im (c (#) f)) . x = Im (c * (f . x)) by P01, A0, VALUED_1:def 5;
P04: ( (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x = (((Im c) (#) (Re f)) . x) + (((Re c) (#) (Im f)) . x) & ((Im c) (#) (Re f)) . x = (Im c) * ((Re f) . x) & ((Re c) (#) (Im f)) . x = (Re c) * ((Im f) . x) ) by P01, A0, B2, A1, VALUED_1:def 1, VALUED_1:def 5;
( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by P01, A0, A1, Def1, Def2;
hence (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x by Q01, P04, COMPLEX1:24; :: thesis: verum

end;

hence Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) by A0, B2, A1, FUNCT_1:9; :: thesis: verum