let D be non empty set ; :: thesis: for p, r being Real
for H being Functional_Sequence of D,REAL holds (r * p) (#) H = r (#) (p (#) H)
let p, r 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 :: 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 RFUNCT_1:17
.= 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