let c be complex number ; :: thesis: for f being PartFunc of REAL ,COMPLEX holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) )
let f be PartFunc of REAL ,COMPLEX ; :: thesis: ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) )
P20: dom (Re (c (#) f)) = dom (c (#) f) by COMSEQ_3:def 3
.= dom f by VALUED_1:def 5 ;
P21: dom (Im (c (#) f)) = dom (c (#) f) by COMSEQ_3:def 4
.= dom f by VALUED_1:def 5 ;
P30: dom ((Re c) (#) (Re f)) = dom (Re f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 3 ;
P31: dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 4 ;
P40: dom ((Im c) (#) (Re f)) = dom (Re f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 3 ;
P41: dom ((Re c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 4 ;
D1: dom (Re (c (#) f)) = (dom f) /\ (dom f) by P20
.= dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) by VALUED_1:12, P30, P31 ;
D2: dom (Im (c (#) f)) = (dom f) /\ (dom f) by P21
.= dom (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) by VALUED_1:def 1, P40, P41 ;

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 AS1: x in dom (Re (c (#) f)) ; :: thesis: (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x
then Q1: ( x in dom (Re f) & x in dom (Im f) ) by P20, COMSEQ_3:def 3, COMSEQ_3:def 4;
thus (Re (c (#) f)) . x = Re ((c (#) f) . x) by COMSEQ_3:def 3, AS1
.= Re (c * (f . x)) by VALUED_1:6
.= ((Re c) * (Re (f . x))) - ((Im c) * (Im (f . x))) by COMPLEX1:24
.= ((Re c) * ((Re f) . x)) - ((Im c) * (Im (f . x))) by Q1, COMSEQ_3:def 3
.= ((Re c) * ((Re f) . x)) - ((Im c) * ((Im f) . x)) by Q1, COMSEQ_3:def 4
.= (((Re c) (#) (Re f)) . x) - ((Im c) * ((Im f) . x)) by VALUED_1:6
.= (((Re c) (#) (Re f)) . x) - (((Im c) (#) (Im f)) . x) by VALUED_1:6
.= (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x by AS1, D1, VALUED_1:13 ; :: thesis: verum

end;

hence Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) by FUNCT_1:9, D1; :: thesis: Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f))

now

let x be set ; :: thesis: ( x in dom (Im (c (#) f)) implies (Im (c (#) f)) . x = (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) . x )
assume AS1: x in dom (Im (c (#) f)) ; :: thesis: (Im (c (#) f)) . x = (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) . x
then Q1: ( x in dom (Re f) & x in dom (Im f) ) by P21, COMSEQ_3:def 3, COMSEQ_3:def 4;
thus (Im (c (#) f)) . x = Im ((c (#) f) . x) by COMSEQ_3:def 4, AS1
.= Im (c * (f . x)) by VALUED_1:6
.= ((Re c) * (Im (f . x))) + ((Im c) * (Re (f . x))) by COMPLEX1:24
.= ((Re c) * ((Im f) . x)) + ((Im c) * (Re (f . x))) by Q1, COMSEQ_3:def 4
.= ((Re c) * ((Im f) . x)) + ((Im c) * ((Re f) . x)) by Q1, COMSEQ_3:def 3
.= (((Re c) (#) (Im f)) . x) + ((Im c) * ((Re f) . x)) by VALUED_1:6
.= (((Re c) (#) (Im f)) . x) + (((Im c) (#) (Re f)) . x) by VALUED_1:6
.= (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) . x by AS1, D2, VALUED_1:def 1 ; :: thesis: verum

end;

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