theorem AP3: :: FINSEQ_9:42

for a, b, c, x, y, z being Complex holds <*a,b,c*> + <*x,y,z*> = <*(a + x),(b + y),(c + z)*>