let a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 be Complex; :: thesis: <*a1,a2,a3,a4,a5*> + <*b1,b2,b3,b4,b5*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5)*>
A1: <*a1,a2,a3,a4*> + <*b1,b2,b3,b4*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4)*> by FINSEQ_9:43;
( <*a1,a2,a3,a4,a5*> = <*a1,a2,a3,a4*> ^ <*a5*> & <*b1,b2,b3,b4,b5*> = <*b1,b2,b3,b4*> ^ <*b5*> ) by FINSEQ_4:75;
then <*a1,a2,a3,a4,a5*> + <*b1,b2,b3,b4,b5*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4)*> ^ <*(a5 + b5)*> by A1, FINSEQ_9:40
.= <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5)*> by FINSEQ_4:75 ;
hence <*a1,a2,a3,a4,a5*> + <*b1,b2,b3,b4,b5*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5)*> ; :: thesis: verum