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

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

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 Def1
.= r (#) (p (#) (H . n)) by VFUNCT_1:14
.= r (#) ((p (#) H) . n) by Def1
.= (r (#) (p (#) H)) . n by Def1 ; :: thesis: verum

end;

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