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 ;
A8: dom (Im (c (#) f)) = (dom f) /\ (dom f) by A2
.= dom (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) by ;
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 ;
thus (Re (c (#) f)) . x = Re ((c (#) f) . x) by
.= 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
.= ((Re c) * ((Re f) . x)) - ((Im c) * ((Im f) . x)) by
.= (((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 ; :: thesis: verum
end;
hence Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) by ; :: 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 ;
thus (Im (c (#) f)) . x = Im ((c (#) f) . x) by
.= 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
.= ((Re c) * ((Im f) . x)) + ((Im c) * ((Re f) . x)) by
.= (((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 ; :: thesis: verum
end;
hence Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) by ; :: thesis: verum