Add fprodunsn to iset.mm

This is a variation of fprodsplitdc intended to be helpful when doing
finite set induction.

Author: jkingdon

iset.mm

@@ -124523,6 +124523,32 @@ seq n ( x. ,
       PQS $.
   $}
 
+  ${
+    $d A j k $.  $d B j k $.  $d V k $.  $d j k ph $.  $d A k $.  $d B k $.
+    $d k ph $.
+    fprodunsn.f $e |- F/_ k D $.
+    fprodunsn.a $e |- ( ph -> A e. Fin ) $.
+    fprodunsn.b $e |- ( ph -> B e. V ) $.
+    fprodunsn.ba $e |- ( ph -> -. B e. A ) $.
+    fprodunsn.ccl $e |- ( ( ph /\ k e. A ) -> C e. CC ) $.
+    fprodunsn.dcl $e |- ( ph -> D e. CC ) $.
+    fprodunsn.d $e |- ( k = B -> C = D ) $.
+    $( Multiply in an additional term in a finite product.  (Contributed by Jim
+       Kingdon, 16-Aug-2024.) $)
+    fprodunsn $p |- ( ph -> prod_ k e. ( A u. { B } ) C
+        = ( prod_ k e. A C x. D ) ) $=
+      ( vj cprod cmul wcel wceq wa csn cun co wn cin c0 disjsn sylibr eqidd cfn
+      unsnfi syl3anc cv wdc simpr orcd df-dc velsn sylib ad2antrr eqneltrd olcd
+      wo biimpi adantl mpjaodan ralrimiva cc adantlr elsni eqeltrd fprodsplitdc
+      elun syl prodsnf syl2anc oveq2d eqtrd ) ABCUAZUBZDFPBDFPZVSDFPZQUCWAEQUCA
+      BVSDVTOFACBRUDZBVSUEUFSKBCUGUHAVTUIABUJRCGRZWCVTUJRIJKBCGUKULAOUMZBRZUNZO
+      VTAWEVTRZTZWFWGWEVSRZWIWFTZWFWFUDZVCZWGWKWFWLWIWFUOUPWFUQZUHWIWJTZWMWGWOW
+      LWFWOWECBWOWJWECSWIWJUOOCURUSAWCWHWJKUTVAVBWNUHWHWFWJVCZAWHWPWEBVSVMVDVEV
+      FVGAFUMZVTRZTZWQBRZDVHRZWQVSRZAWTXAWRLVIWSXBTZDEVHXCWQCSZDESXBXDWSWQCVJVE
+      NVNAEVHRZWRXBMUTVKWRWTXBVCZAWRXFWQBVSVMVDVEVFVLAWBEWAQAWDXEWBESJMDEFCGHNV
+      OVPVQVR $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#