let a1, a2, a3, a4, a5, a6, a7, a8, b1, b2, b3, b4, b5, b6, b7, b8 be Complex; :: thesis: <*a1,a2,a3,a4,a5,a6,a7,a8*> + <*b1,b2,b3,b4,b5,b6,b7,b8*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5),(a6 + b6),(a7 + b7),(a8 + b8)*>
A1: <*a1,a2,a3,a4,a5*> + <*b1,b2,b3,b4,b5*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5)*> by A5B5;
( <*a1,a2,a3,a4,a5,a6,a7,a8*> = <*a1,a2,a3,a4,a5*> ^ <*a6,a7,a8*> & <*b1,b2,b3,b4,b5,b6,b7,b8*> = <*b1,b2,b3,b4,b5*> ^ <*b6,b7,b8*> ) by AOFA_A00:def 6;
then <*a1,a2,a3,a4,a5,a6,a7,a8*> + <*b1,b2,b3,b4,b5,b6,b7,b8*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5)*> ^ <*(a6 + b6),(a7 + b7),(a8 + b8)*> by A1, FINSEQ940B;
hence <*a1,a2,a3,a4,a5,a6,a7,a8*> + <*b1,b2,b3,b4,b5,b6,b7,b8*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5),(a6 + b6),(a7 + b7),(a8 + b8)*> by AOFA_A00:def 6; :: thesis: verum