f is FinSequence of REAL by FINSEQ_1:102;
hence (f | n) /^ n is empty ; :: thesis: verum