set f = primesFinS 1;
A1: len (primesFinS 1) = 1 by Def1;
(primesFinS 1) . (0 + 1) = 2 by Def1, MOEBIUS2:8;
hence primesFinS 1 = <*2*> by A1, FINSEQ_1:40; :: thesis: verum