let a, b, c, d, x, y, z, v be Complex; <*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; verum