theorem :: SEQFUNC2:22

for D being non empty set
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
( ||.H.|| # x = ||.(H # x).|| & (- H) # x = (- 1) * (H # x) ) by Th28;