for i being Element of NAT
for x, y being FinSequence of COMPLEX st i in dom (x + y) holds
(x + y) . i = (x . i) + (y . i) by VALUED_1:def 1;