Add fprodfac to iset.mm

Stated as in set.mm.  The proof is by induction rather than by referring
to seq .

Author: jkingdon

iset.mm

@@ -124691,6 +124691,26 @@ seq n ( x. ,
       fprodcllemf ) AHIBCJDEJKLAMNHOZJPIOZJPQUDUERSJPAUDUETUAFGAUBUC $.
   $}
 
+  ${
+    $d A k w x $.
+    $( Factorial using product notation.  (Contributed by Scott Fenton,
+       15-Dec-2017.) $)
+    fprodfac $p |- ( A e. NN0 -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k ) $=
+      ( vw vx cv cfa cfv c1 cfz co cprod cc0 caddc fveq2 oveq2 prodeq1d eqeq12d
+      wceq wcel cmul c0 prod0 fz10 prodeq1i fac0 3eqtr4ri cn0 cn wo wi elnn0 wa
+      simpr oveq1d wb nnnn0 facp1 syl cuz elnnuz biimpi cc elfzelz zcnd fprodp1
+      adantl id adantr mpbird ex cz 1zzd 1cnd fprod1 syl2anc oveq1 0p1e1 eqtrdi
+      oveq2d fv0p1e1 fac1 3eqtr4rd a1d jaoi sylbi nn0ind ) CEZFGZHWGIJZBEZBKZRL
+      FGZHLIJZWJBKZRDEZFGZHWOIJZWJBKZRZWOHMJZFGZHWTIJZWJBKZRZAFGZHAIJZWJBKZRCDA
+      WGLRZWHWLWKWNWGLFNXHWIWMWJBWGLHIOPQWGWORZWHWPWKWRWGWOFNXIWIWQWJBWGWOHIOPQ
+      WGWTRZWHXAWKXCWGWTFNXJWIXBWJBWGWTHIOPQWGARZWHXEWKXGWGAFNXKWIXFWJBWGAHIOPQ
+      UAWJBKHWNWLWJBUBWMUAWJBUCUDUEUFWOUGSZWOUHSZWOLRZUIWSXDUJZWOUKXMXOXNXMWSXD
+      XMWSULZXDWPWTTJZWRWTTJZRZXPWPWRWTTXMWSUMUNXMXDXSUOWSXMXAXQXCXRXMXLXAXQRWO
+      UPWOUQURXMWJWTBHWOXMWOHUSGSWOUTVAWJXBSZWJVBSXMXTWJWJHWTVCVDVFWJWTRVGVEQVH
+      VIVJXNXDWSXNHHIJZWJBKZHXCXAXNHVKSHVBSYBHRXNVLXNVMWJHBHWJHRVGVNVOXNXBYAWJB
+      XNWTHHIXNWTLHMJHWOLHMVPVQVRVSPXNXAHFGHFWOVTWAVRWBWCWDWEWF $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#