let X be RealLinearSpace-Sequence; :: thesis: 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 ) )
let v, w be Element of product (carr X); :: thesis: 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 ) )
let i be Element of dom (carr X); :: thesis: ( ([:(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 ) )
([:(addop X):] . (v,w)) . i = ((addop X) . i) . ((v . i),(w . i)) by PRVECT_1:def 8;
hence ( ([:(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 ) ) by PRVECT_1:def 12; :: thesis: verum