theorem :: MATRIXC1:30

for x being FinSequence of REAL
for y being FinSequence of COMPLEX st x = y & len x >= 1 holds
Sum x = Sum y ;