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

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

end;

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