theorem Th61: :: COMPLSP2:72

for x, y1, y2 being FinSequence of COMPLEX st len x = len y1 & len y1 = len y2 holds
|(x,(y1 - y2))| = |(x,y1)| - |(x,y2)|