let seq be Complex_Sequence; :: thesis: for z being Complex holds
( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) )
let z be Complex; :: thesis: ( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) )

now :: thesis: for n being Element of NAT holds (Re (z (#) seq)) . n = (((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq))) . n

let n be Element of NAT ; :: thesis: (Re (z (#) seq)) . n = (((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq))) . n
thus (Re (z (#) seq)) . n = Re ((z (#) seq) . n) by Def5
.= Re (z * (seq . n)) by VALUED_1:6
.= Re ((((Re z) * (Re (seq . n))) - ((Im z) * (Im (seq . n)))) + ((((Re z) * (Im (seq . n))) + ((Re (seq . n)) * (Im z))) * <i>)) by COMPLEX1:82
.= ((Re z) * (Re (seq . n))) - ((Im z) * (Im (seq . n))) by COMPLEX1:12
.= ((Re z) * ((Re seq) . n)) - ((Im z) * (Im (seq . n))) by Def5
.= ((Re z) * ((Re seq) . n)) - ((Im z) * ((Im seq) . n)) by Def6
.= (((Re z) (#) (Re seq)) . n) - ((Im z) * ((Im seq) . n)) by SEQ_1:9
.= (((Re z) (#) (Re seq)) . n) - (((Im z) (#) (Im seq)) . n) by SEQ_1:9
.= (((Re z) (#) (Re seq)) . n) + (- (((Im z) (#) (Im seq)) . n))
.= (((Re z) (#) (Re seq)) . n) + ((- ((Im z) (#) (Im seq))) . n) by SEQ_1:10
.= (((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq))) . n by SEQ_1:7 ; :: thesis: verum

end;

hence Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) ; :: thesis: Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq))

now :: thesis: for n being Element of NAT holds (Im (z (#) seq)) . n = (((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq))) . n

let n be Element of NAT ; :: thesis: (Im (z (#) seq)) . n = (((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq))) . n
thus (Im (z (#) seq)) . n = Im ((z (#) seq) . n) by Def6
.= Im (z * (seq . n)) by VALUED_1:6
.= Im ((((Re z) * (Re (seq . n))) - ((Im z) * (Im (seq . n)))) + ((((Re z) * (Im (seq . n))) + ((Re (seq . n)) * (Im z))) * <i>)) by COMPLEX1:82
.= ((Re z) * (Im (seq . n))) + ((Re (seq . n)) * (Im z)) by COMPLEX1:12
.= ((Re z) * (Im (seq . n))) + ((Im z) * ((Re seq) . n)) by Def5
.= ((Re z) * ((Im seq) . n)) + ((Im z) * ((Re seq) . n)) by Def6
.= (((Re z) (#) (Im seq)) . n) + ((Im z) * ((Re seq) . n)) by SEQ_1:9
.= (((Re z) (#) (Im seq)) . n) + (((Im z) (#) (Re seq)) . n) by SEQ_1:9
.= (((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq))) . n by SEQ_1:7 ; :: thesis: verum

end;

hence Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) ; :: thesis: verum