theorem Th30: :: COMPLSP2:36
for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds
(x - y) - z = x - (y + z)