theorem :: FINSEQ_9:43

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