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

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

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

end;

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