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

now

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:21
.= p * (seq . (Ns . n)) by SEQ_1:13
.= p * ((seq * Ns) . n) by FUNCT_2:21
.= (p (#) (seq * Ns)) . n by SEQ_1:13 ; :: thesis: verum

end;

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