let k, m, n be Nat; :: thesis: ( 1 <= k & k <= m & m <= n implies card (PrimeDivisors (Product (mid ((primesFinS n),k,m)))) = (m - k) + 1 )
assume A1: ( 1 <= k & k <= m & m <= n ) ; :: thesis: card (PrimeDivisors (Product (mid ((primesFinS n),k,m)))) = (m - k) + 1
set M = mid ((primesFinS n),k,m);
A2: len (primesFinS n) = n by NUMBER13:def 1;
( 1 <= m & k <= n ) by A1, XXREAL_0:2;
then len (mid ((primesFinS n),k,m)) = (m -' k) + 1 by A1, A2, FINSEQ_6:118;
then A3: dom (mid ((primesFinS n),k,m)) = Seg ((m -' k) + 1) by FINSEQ_1:def 3;
A4: card (rng (mid ((primesFinS n),k,m))) = card (dom (mid ((primesFinS n),k,m))) by CARD_1:70;
PrimeDivisors (Product (mid ((primesFinS n),k,m))) = rng (mid ((primesFinS n),k,m)) by A1, Th7;
hence card (PrimeDivisors (Product (mid ((primesFinS n),k,m)))) = (m - k) + 1 by A3, A4, A1, XREAL_1:233; :: thesis: verum