let seq be Complex_Sequence; :: thesis: for Nseq being increasing sequence of NAT holds
( Re (seq * Nseq) = (Re seq) * Nseq & Im (seq * Nseq) = (Im seq) * Nseq )
let Nseq be increasing sequence of NAT ; :: thesis: ( Re (seq * Nseq) = (Re seq) * Nseq & Im (seq * Nseq) = (Im seq) * Nseq )

now

let n be Element of NAT ; :: thesis: (Re (seq * Nseq)) . n = ((Re seq) * Nseq) . n
thus (Re (seq * Nseq)) . n = Re ((seq * Nseq) . n) by Def3
.= Re (seq . (Nseq . n)) by FUNCT_2:21
.= (Re seq) . (Nseq . n) by Def3
.= ((Re seq) * Nseq) . n by FUNCT_2:21 ; :: thesis: verum

end;

hence Re (seq * Nseq) = (Re seq) * Nseq by FUNCT_2:113; :: thesis: Im (seq * Nseq) = (Im seq) * Nseq

now

let n be Element of NAT ; :: thesis: (Im (seq * Nseq)) . n = ((Im seq) * Nseq) . n
thus (Im (seq * Nseq)) . n = Im ((seq * Nseq) . n) by Def4
.= Im (seq . (Nseq . n)) by FUNCT_2:21
.= (Im seq) . (Nseq . n) by Def4
.= ((Im seq) * Nseq) . n by FUNCT_2:21 ; :: thesis: verum

end;

hence Im (seq * Nseq) = (Im seq) * Nseq by FUNCT_2:113; :: thesis: verum