theorem Th11: :: LOPBAN15:9

for X being RealLinearSpace-Sequence
for v, w being Element of product (carr X)
for i being Element of dom (carr X) holds
( ([:(addop X):] . (v,w)) . i = the addF of (X . i) . ((v . i),(w . i)) & ( for vi, wi being VECTOR of (X . i) st vi = v . i & wi = w . i holds
([:(addop X):] . (v,w)) . i = vi + wi ) )