theorem AP2: :: FINSEQ_9:41

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