let r, p be Real; :: thesis: for seq being Real_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)
let seq be Real_Sequence; :: thesis: (r * p) (#) seq = r (#) (p (#) seq)

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

let n be Element of NAT ; :: thesis: ((r * p) (#) seq) . n = (r (#) (p (#) seq)) . n
thus ((r * p) (#) seq) . n = (r * p) * (seq . n) by Th9
.= r * (p * (seq . n))
.= r * ((p (#) seq) . n) by Th9
.= (r (#) (p (#) seq)) . n by Th9 ; :: thesis: verum

end;

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