let c be Complex; :: 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)) )
A1: dom (Re (c (#) f)) = dom (c (#) f) by COMSEQ_3:def 3
.= dom f by VALUED_1:def 5 ;
A2: dom (Im (c (#) f)) = dom (c (#) f) by COMSEQ_3:def 4
.= dom f by VALUED_1:def 5 ;
A3: dom ((Re c) (#) (Re f)) = dom (Re f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 3 ;
A4: dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 4 ;
A5: dom ((Im c) (#) (Re f)) = dom (Re f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 3 ;
A6: dom ((Re c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5
.= dom f by COMSEQ_3:def 4 ;
A7: dom (Re (c (#) f)) = (dom f) /\ (dom f) by A1
.= dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) by A3, A4, VALUED_1:12 ;
A8: dom (Im (c (#) f)) = (dom f) /\ (dom f) by A2
.= dom (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) by A5, A6, VALUED_1:def 1 ;

now :: thesis: for x being object st x in dom (Re (c (#) f)) holds
(Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x

let x be object ; :: thesis: ( x in dom (Re (c (#) f)) implies (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x )
assume A9: x in dom (Re (c (#) f)) ; :: thesis: (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x
then A10: ( x in dom (Re f) & x in dom (Im f) ) by A1, COMSEQ_3:def 3, COMSEQ_3:def 4;
thus (Re (c (#) f)) . x = Re ((c (#) f) . x) by A9, COMSEQ_3:def 3
.= Re (c * (f . x)) by VALUED_1:6
.= ((Re c) * (Re (f . x))) - ((Im c) * (Im (f . x))) by COMPLEX1:9
.= ((Re c) * ((Re f) . x)) - ((Im c) * (Im (f . x))) by A10, COMSEQ_3:def 3
.= ((Re c) * ((Re f) . x)) - ((Im c) * ((Im f) . x)) by A10, 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 A9, A7, VALUED_1:13 ; :: thesis: verum

end;

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

now :: thesis: for x being object st x in dom (Im (c (#) f)) holds
(Im (c (#) f)) . x = (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) . x

let x be object ; :: thesis: ( x in dom (Im (c (#) f)) implies (Im (c (#) f)) . x = (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) . x )
assume A11: x in dom (Im (c (#) f)) ; :: thesis: (Im (c (#) f)) . x = (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) . x
then A12: ( x in dom (Re f) & x in dom (Im f) ) by A2, COMSEQ_3:def 3, COMSEQ_3:def 4;
thus (Im (c (#) f)) . x = Im ((c (#) f) . x) by A11, COMSEQ_3:def 4
.= Im (c * (f . x)) by VALUED_1:6
.= ((Re c) * (Im (f . x))) + ((Im c) * (Re (f . x))) by COMPLEX1:9
.= ((Re c) * ((Im f) . x)) + ((Im c) * (Re (f . x))) by A12, COMSEQ_3:def 4
.= ((Re c) * ((Im f) . x)) + ((Im c) * ((Re f) . x)) by A12, 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 A11, A8, VALUED_1:def 1 ; :: thesis: verum

end;

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