let G be RealLinearSpace-Sequence; :: thesis: for v1, w1 being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:(addop G):] . v1,w1) . i = the addF of (G . i) . (v1 . i),(w1 . i) & ( for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds
([:(addop G):] . v1,w1) . i = vi + wi ) )
let v1, w1 be Element of product (carr G); :: thesis: for i being Element of dom (carr G) holds
( ([:(addop G):] . v1,w1) . i = the addF of (G . i) . (v1 . i),(w1 . i) & ( for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds
([:(addop G):] . v1,w1) . i = vi + wi ) )
let i be Element of dom (carr G); :: thesis: ( ([:(addop G):] . v1,w1) . i = the addF of (G . i) . (v1 . i),(w1 . i) & ( for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds
([:(addop G):] . v1,w1) . i = vi + wi ) )
([:(addop G):] . v1,w1) . i = ((addop G) . i) . (v1 . i),(w1 . i) by PRVECT_1:def 10;
hence ( ([:(addop G):] . v1,w1) . i = the addF of (G . i) . (v1 . i),(w1 . i) & ( for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds
([:(addop G):] . v1,w1) . i = vi + wi ) ) by Def5; :: thesis: verum