let D be non empty set ; :: thesis: for r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
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 Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H holds
(r (#) H) # x = r * (H # x)
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y
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, the carrier of Y; :: 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 VFUNCT_1:def 4;
X2: (r (#) H) . n = r (#) (H . n) by Def1;
thus ((r (#) H) # x) . n = ((r (#) H) . n) /. x by Def10
.= r * ((H . n) /. x) by X2, A2, VFUNCT_1:def 4
.= r * ((H # x) . n) by Def10
.= (r * (H # x)) . n by NORMSP_1:def 5 ; :: thesis: verum
end;
hence (r (#) H) # x = r * (H # x) by FUNCT_2:63; :: thesis: verum