<*a1,a2,a3,a4,a5,a6,a7*> ^ <*a8*> = (<*a1,a2,a3,a4,a5*> ^ <*a6,a7*>) ^ <*a8*> by AOFA_A00:def 5
.= <*a1,a2,a3,a4,a5*> ^ <*a6,a7,a8*> by FINSEQ_1:32 ;
hence <*a1,a2,a3,a4,a5,a6,a7,a8*> is complex-valued by AOFA_A00:def 6; :: thesis: verum