Adds singleton and not indiscrete with multiple points

Author: GeoffreySangston

theorems/T000881.md

@@ -0,0 +1,17 @@
+---
+uid: T000881
+if:
+  and:
+  - P000058: false
+  - P000129: true
+then:
+  P000238: true
+refs:
+- mathse: 541116
+  name: Answer to "Cardinality of a vector space versus the cardinality of its basis"
+---
+
+The vector space $V$ of finite formal linear combinations of elements from $X$ over $\mathbb{R}$ has the 
+same cardinality as $X$; see {{mathse:541116}}. Hence there exists a bijection
+$X \to V$. With the indiscrete topology $V$ is a real TVS,
+and this bijection is a homeomorphism

theorems/T000882.md

@@ -0,0 +1,11 @@
+---
+uid: T000882
+if:
+  and:
+  - P000125: false
+  - P000137: false
+then:
+  P000238: true
+---
+
+The addition and scalar multiplication are uniquely determined on the singleton. These are continuous since they are constant maps, and satisfy the axioms of a vector space.