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