theorem Th55: :: COMPLSP2:66

for x1, x2, y being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len y holds
|((x1 + x2),y)| = |(x1,y)| + |(x2,y)|