let D be non empty set ; :: thesis: for r, p being Real
for H being Functional_Sequence of D,REAL holds (r * p) (#) H = r (#) (p (#) H)
let r, p be Real; :: thesis: for H being Functional_Sequence of D,REAL holds (r * p) (#) H = r (#) (p (#) H)
let H be Functional_Sequence of D,REAL; :: thesis: (r * p) (#) H = r (#) (p (#) H)

now

let n be Element of NAT ; :: thesis: ((r * p) (#) H) . n = (r (#) (p (#) H)) . n
thus ((r * p) (#) H) . n = (r * p) (#) (H . n) by Def2
.= r (#) (p (#) (H . n)) by RFUNCT_1:17
.= r (#) ((p (#) H) . n) by Def2
.= (r (#) (p (#) H)) . n by Def2 ; :: thesis: verum

end;

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