let K be Ring; for G being VectorSpace-Sequence of K
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 G be VectorSpace-Sequence of K; 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); 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); ( ([:(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 8;
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 PRVECT_1:def 12; verum