A1: 12 (#) (f | (s - 1)) = (12 (#) f) | (s - 1) by Th56;
len (12 (#) f) = s + 1 by CARD_1:def 7;
then A2: len (12 (#) (f | (s - 1))) = s - 1 by A1, FINSEQ_1:59, XREAL_1:6;
len <*(15 * (f . s)),(20 * (f . s)),(12 * (f . (s + 1)))*> = 3 by FINSEQ_1:45;
then len (SierpProblem168FS f) = (s - 1) + 3 by A2, FINSEQ_1:22;
hence SierpProblem168FS f is (s + 1) + 1 -element ; :: thesis: verum