let D be non empty set ; :: thesis: for r being Real
for H being Functional_Sequence of D,REAL st r <> 0 holds
(r (#) H) " = (r ") (#) (H ")
let r be Real; :: thesis: for H being Functional_Sequence of D,REAL st r <> 0 holds
(r (#) H) " = (r ") (#) (H ")
let H be Functional_Sequence of D,REAL; :: thesis: ( r <> 0 implies (r (#) H) " = (r ") (#) (H ") )
assume A1: r <> 0 ; :: thesis: (r (#) H) " = (r ") (#) (H ")

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

let n be Element of NAT ; :: thesis: ((r (#) H) ") . n = ((r ") (#) (H ")) . n
thus ((r (#) H) ") . n = ((r (#) H) . n) ^ by Def2
.= (r (#) (H . n)) ^ by Def1
.= (r ") (#) ((H . n) ^) by A1, RFUNCT_1:28
.= (r ") (#) ((H ") . n) by Def2
.= ((r ") (#) (H ")) . n by Def1 ; :: thesis: verum

end;

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