Add prodsns to iset.mm

Copied without change from set.mm.

Author: jkingdon

iset.mm

@@ -124512,6 +124512,17 @@ seq n ( x. ,
       UIUOBUQCHHBUJZVDVETVAUSUTPURBUQCHVFVDVETUKUL $.
   $}
 
+  ${
+    $d A n $.  $d k n $.  $d M k $.  $d M n $.  $d V n $.
+    $( A product of the singleton is the term.  (Contributed by Scott Fenton,
+       25-Dec-2017.) $)
+    prodsns $p |- ( ( M e. V /\ [_ M / k ]_ A e. CC ) ->
+       prod_ k e. { M } A = [_ M / k ]_ A ) $=
+      ( vn wcel csb cc wa csn cprod nfcv nfcsb1v csbeq1a cbvprodi csbeq1 prodsn
+      cv syl5eq ) CDFBCAGZHFICJZABKUABERZAGZEKTUAAUCBEEALBUBAMBUBANOUCTECDBUBCA
+      PQS $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#