theorem Th25: :: COMPLSP2:30

for c being Complex
for x, y being FinSequence of COMPLEX st len x = len y holds
c * (x + y) = (c * x) + (c * y)