let n be Nat; :: thesis: Product (primesFinS (n + 1)) = (Product (primesFinS n)) * (primenumber n)
len (primesFinS (n + 1)) = n + 1 by NUMBER13:def 1;
then A1: primesFinS (n + 1) = ((primesFinS (n + 1)) | n) ^ <*((primesFinS (n + 1)) . (n + 1))*> by FINSEQ_3:55;
A2: n < n + 1 by NAT_1:13;
then A3: (primesFinS (n + 1)) | n = primesFinS n by NUMBER13:17;
(primesFinS (n + 1)) . (n + 1) = primenumber n by A2, NUMBER13:def 1;
then primesFinS (n + 1) = (primesFinS n) ^ <*(primenumber n)*> by A1, A3;
then Product (primesFinS (n + 1)) = (Product (primesFinS n)) * (primenumber n) by RVSUM_1:96;
hence Product (primesFinS (n + 1)) = (Product (primesFinS n)) * (primenumber n) ; :: thesis: verum