let D be non empty set ; :: thesis: for Y being RealNormSpace
for H1, H2 being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H1 & X common_on_dom H2 holds
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )
let Y be RealNormSpace; :: thesis: for H1, H2 being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H1 & X common_on_dom H2 holds
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )
let H1, H2 be Functional_Sequence of D, the carrier of Y; :: thesis: for X being set st X common_on_dom H1 & X common_on_dom H2 holds
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )
let X be set ; :: thesis: ( X common_on_dom H1 & X common_on_dom H2 implies for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x ) )
assume A1: ( X common_on_dom H1 & X common_on_dom H2 ) ; :: thesis: for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )
let x be Element of D; :: thesis: ( x in X implies ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x ) )
assume x in X ; :: thesis: ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )
then ( {x} common_on_dom H1 & {x} common_on_dom H2 ) by A1, Th25;
hence ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x ) by Th27; :: thesis: verum