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:13;