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 :: thesis: for n being Element of NAT holds ((r (#) H) # x) . n = (r (#) (H # x)) . n
let n be Element of NAT ; :: thesis: ((r (#) H) # x) . n = (r (#) (H # x)) . n
( x in {x} & {x} c= dom (H . n) ) by A1, TARSKI:def 1;
then x in dom (H . n) ;
then A2: x in dom (r (#) (H . n)) by VALUED_1:def 5;
thus ((r (#) H) # x) . n = ((r (#) H) . n) . x by Def10
.= (r (#) (H . n)) . x by Def1
.= r * ((H . n) . x) by A2, VALUED_1:def 5
.= r * ((H # x) . n) by Def10
.= (r (#) (H # x)) . n by SEQ_1:9 ; :: thesis: verum
end;
hence (r (#) H) # x = r (#) (H # x) by FUNCT_2:63; :: thesis: verum