theorem Th17: :: COMPLSP2:21
for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
(x1 - x2) *' = (x1 *') - (x2 *')