let D be non empty set ; :: thesis: for r being Real
for H being Functional_Sequence of D,REAL
for x being Element of D st {x} common_on_dom H holds
(r (#) H) # x = r (#) (H # x)
let r be Real; :: thesis: for H being Functional_Sequence of D,REAL
for x being Element of D st {x} common_on_dom H holds
(r (#) H) # x = r (#) (H # x)
let H be Functional_Sequence of D,REAL ; :: thesis: for x being Element of D st {x} common_on_dom H holds
(r (#) H) # x = r (#) (H # x)
let x be Element of D; :: thesis: ( {x} common_on_dom H implies (r (#) H) # x = r (#) (H # x) )
assume A1: {x} common_on_dom H ; :: thesis: (r (#) H) # x = r (#) (H # x)

now

let n be Element of NAT ; :: thesis: ((r (#) H) # x) . n = (r (#) (H # x)) . n
A2: x in {x} by TARSKI:def 1;
{x} c= dom (H . n) by A1, Def10;
then x in dom (H . n) by A2;
then A3: x in dom (r (#) (H . n)) by VALUED_1:def 5;
thus ((r (#) H) # x) . n = ((r (#) H) . n) . x by Def11
.= (r (#) (H . n)) . x by Def2
.= r * ((H . n) . x) by A3, VALUED_1:def 5
.= r * ((H # x) . n) by Def11
.= (r (#) (H # x)) . n by SEQ_1:13 ; :: thesis: verum

end;

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