let g be Complex; :: thesis: for seq being Complex_Sequence
for Ns being increasing sequence of NAT holds (g (#) seq) * Ns = g (#) (seq * Ns)
let seq be Complex_Sequence; :: thesis: for Ns being increasing sequence of NAT holds (g (#) seq) * Ns = g (#) (seq * Ns)
let Ns be increasing sequence of NAT; :: thesis: (g (#) seq) * Ns = g (#) (seq * Ns)

now :: thesis: for n being Element of NAT holds ((g (#) seq) * Ns) . n = (g (#) (seq * Ns)) . n

let n be Element of NAT ; :: thesis: ((g (#) seq) * Ns) . n = (g (#) (seq * Ns)) . n
thus ((g (#) seq) * Ns) . n = (g (#) seq) . (Ns . n) by FUNCT_2:15
.= g * (seq . (Ns . n)) by VALUED_1:6
.= g * ((seq * Ns) . n) by FUNCT_2:15
.= (g (#) (seq * Ns)) . n by VALUED_1:6 ; :: thesis: verum

end;

hence (g (#) seq) * Ns = g (#) (seq * Ns) by FUNCT_2:63; :: thesis: verum