reconsider f = <*a,b,c*> as complex-valued FinSequence ;
f ^ <*d*> is complex-valued ;
hence <*a,b,c,d*> is complex-valued by FINSEQ_4:def 7; :: thesis: verum