Add dvbss to iset.mm

Stated as in set.mm.  The proof is very similar to the set.mm proof, but
just needs small changes for the notation of the topology on complex
numbers.

Author: jkingdon

iset.mm

@@ -136576,6 +136576,17 @@ S C_ ( P ( ball ` D ) T ) ) $=
         OUIVGUKOUCULUMZVBVETZVCVFTACRTBRDUNBCTVIVJUOGHILMNBCEDFJKUPUQVBVEURUSVD
         RUTVA $.
     $}
+
+    $( The set of differentiable points is a subset of the domain of the
+       function.  (Contributed by Mario Carneiro, 6-Aug-2014.)  (Revised by
+       Mario Carneiro, 9-Feb-2015.) $)
+    dvbss $p |- ( ph -> dom ( S _D F ) C_ A ) $=
+      ( cdv co cdm cabs cfv eqid ctop wcel wss cvv cc sylancr ctopon cmin cmopn
+      ccom crest dvbssntrcntop cuni cntoptop cnex ssexg sylancl wceq cntoptopon
+      cnt resttop resttopon toponuni syl sseqtrd ntrss2 syl2anc sstrd ) ACDHIJB
+      KUAUCUBLZCUDIZUMLLZBABCDVCVBEFGVCMVBMZUEAVCNOZBVCUFZPVDBPAVBNOCQOZVFVBVEU
+      GACRPZRQOVHEUHCRQUIUJCVBQUNSABCVGGAVCCTLOZCVGUKAVBRTLOVIVJVBVEULECVBRUOSC
+      VCUPUQURBVCVGVGMUSUTVA $.
   $}