len f = n by FINSEQ_3:153;
hence (f ^ <*a*>) | n = f ; :: thesis: verum