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 set st X common_on_dom H holds
for x being Element of D st x in X 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 set st X common_on_dom H holds
for x being Element of D st x in X 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 set st X common_on_dom H holds
for x being Element of D st x in X holds
(r (#) H) # x = r * (H # x)
let H be Functional_Sequence of D, the carrier of Y; :: thesis: for X being set st X common_on_dom H holds
for x being Element of D st x in X holds
(r (#) H) # x = r * (H # x)
let X be set ; :: thesis: ( X common_on_dom H implies for x being Element of D st x in X holds
(r (#) H) # x = r * (H # x) )
assume A1: X common_on_dom H ; :: thesis: for x being Element of D st x in X holds
(r (#) H) # x = r * (H # x)
let x be Element of D; :: thesis: ( x in X implies (r (#) H) # x = r * (H # x) )
assume x in X ; :: thesis: (r (#) H) # x = r * (H # x)
then {x} common_on_dom H by A1, Th25;
hence (r (#) H) # x = r * (H # x) by Th29; :: thesis: verum