A1:
0 + 1 <= s
by NAT_1:13;
A2:
len f = s + 1
by CARD_1:def 7;
s <= s + 1
by NAT_1:11;
then
s in dom f
by A1, A2, FINSEQ_3:25;
then A3:
f . s in rng f
by FUNCT_1:def 3;
1 <= s + 1
by NAT_1:11;
then
s + 1 in dom f
by A2, FINSEQ_3:25;
then
f . (s + 1) in rng f
by FUNCT_1:def 3;
hence
SierpProblem168FS f is non-empty
by A3; verum