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 :: thesis: for n being Element of NAT holds (Re (seq * Nseq)) . n = ((Re seq) * Nseq) . n

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 Def5
.= Re (seq . (Nseq . n)) by FUNCT_2:15
.= (Re seq) . (Nseq . n) by Def5
.= ((Re seq) * Nseq) . n by FUNCT_2:15 ; :: thesis: verum

end;

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

now :: thesis: for n being Element of NAT holds (Im (seq * Nseq)) . n = ((Im seq) * Nseq) . n

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 Def6
.= Im (seq . (Nseq . n)) by FUNCT_2:15
.= (Im seq) . (Nseq . n) by Def6
.= ((Im seq) * Nseq) . n by FUNCT_2:15 ; :: thesis: verum

end;

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