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