theorem Th36: :: COMPLSP2:43

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