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