<*a1,a2,a3,a4*> ^ <*a5*> is complex-valued ;
hence <*a1,a2,a3,a4,a5*> is complex-valued by FINSEQ_4:75; :: thesis: verum