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