theorem Th24: :: COMPLSP2:28

for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds
x + (y + z) = (x + y) + z