let r, p be real number ; :: 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

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 Th13
.= r * (p * (seq . n))
.= r * ((p (#) seq) . n) by Th13
.= (r (#) (p (#) seq)) . n by Th13 ; :: thesis: verum

end;

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