let a, b, c, d, x, y, z, v be Complex; :: thesis: <*a,b,c,d*> + <*x,y,z,v*> = <*(a + x),(b + y),(c + z),(d + v)*>
reconsider f = <*a,b,c*> as 3 -element complex-valued FinSequence ;
reconsider g = <*x,y,z*> as 3 -element complex-valued FinSequence ;
( <*a,b,c,d*> = f ^ <*d*> & <*x,y,z,v*> = g ^ <*v*> ) by FINSEQ_4:def 7;
then <*a,b,c,d*> + <*x,y,z,v*> = (f + g) ^ <*(d + v)*> by FPA
.= <*(a + x),(b + y),(c + z)*> ^ <*(d + v)*> by AP3 ;
hence <*a,b,c,d*> + <*x,y,z,v*> = <*(a + x),(b + y),(c + z),(d + v)*> by FINSEQ_4:def 7; :: thesis: verum