let p be Real; :: thesis: for seq being Real_Sequence
for Ns being increasing sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns)
let seq be Real_Sequence; :: thesis: for Ns being increasing sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns)
let Ns be increasing sequence of NAT; :: thesis: (p (#) seq) * Ns = p (#) (seq * Ns)

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

let n be Element of NAT ; :: thesis: ((p (#) seq) * Ns) . n = (p (#) (seq * Ns)) . n
thus ((p (#) seq) * Ns) . n = (p (#) seq) . (Ns . n) by FUNCT_2:15
.= p * (seq . (Ns . n)) by SEQ_1:9
.= p * ((seq * Ns) . n) by FUNCT_2:15
.= (p (#) (seq * Ns)) . n by SEQ_1:9 ; :: thesis: verum

end;

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