A1: ex D being non empty set st f is FinSequence of D by Th0;
0 + (len f) <= n + (len f) by XREAL_1:6;
hence f /^ ((len f) + n) is empty by A1, FINSEQ_5:32; :: thesis: verum