let a, b, x, y be Complex; :: thesis: <*a,b*> + <*x,y*> = <*(a + x),(b + y)*>
<*a,b*> + <*x,y*> = (<*a*> + <*x*>) ^ <*(b + y)*> by FPA;
hence <*a,b*> + <*x,y*> = <*(a + x),(b + y)*> by APB; :: thesis: verum