Add fprodcllem to iset.mm

Stated as in set.mm.  The proof needs a little intuitionizing but is
mostly unchanged from the set.mm proof.

Author: jkingdon

iset.mm

@@ -124586,6 +124586,17 @@ seq n ( x. ,
         PVRVCUUJXQUUEUUOUUPWQYMXQVFYMUUEXQUUGWBUUNUUPXPUULTURZFNUBUCXPYOFFUUKXP
         PUUMUVAFUUKXPUULTWNRUULYOPUVAYPFUULYOXPTWORWRVHWSWJWKWLXCJWTXAXB $.
     $}
+
+    $d A k x y $.  $d A w $.  $d B x y $.  $d S k x y $.  $d k ph x y $.
+    fprodcllem.5 $e |- ( ph -> 1 e. S ) $.
+    $( Finite product closure lemma.  (Contributed by Scott Fenton,
+       14-Dec-2017.) $)
+    fprodcllem $p |- ( ph -> prod_ k e. A B e. S ) $=
+      ( vw c0 wceq wcel wa c1 adantr cv cprod wne prodeq1 eqtrdi adantl eqeltrd
+      prod0 cc wss cmul co adantlr cfn simpr fprodcl2lem wex wo fin0or n0r 3syl
+      orim2i mpjaodan ) ADNOZDEGUAZFPDNUBZAVCQVDRFVCVDROAVCVDNEGUARDNEGUCEGUGUD
+      UEARFPVCLSUFAVEQBCDEFGAFUHUIVEHSABTZFPCTZFPQVFVGUJUKFPVEIULADUMPZVEJSAGTD
+      PEFPVEKULAVEUNUOAVHVCMTDPMUPZUQVCVEUQJMDURVIVEVCMDUSVAUTVB $.
   $}