let G be RealLinearSpace-Sequence; :: thesis: for v1, w1 being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:():] . (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
([:():] . (v1,w1)) . i = vi + wi ) )

let v1, w1 be Element of product (carr G); :: thesis: for i being Element of dom (carr G) holds
( ([:():] . (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
([:():] . (v1,w1)) . i = vi + wi ) )

let i be Element of dom (carr G); :: thesis: ( ([:():] . (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
([:():] . (v1,w1)) . i = vi + wi ) )

([:():] . (v1,w1)) . i = (() . i) . ((v1 . i),(w1 . i)) by PRVECT_1:def 8;
hence ( ([:():] . (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
([:():] . (v1,w1)) . i = vi + wi ) ) by Def5; :: thesis: verum