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