diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Analysis/Euclidean_Space.thy
--- a/src/HOL/Analysis/Euclidean_Space.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -53,6 +53,9 @@
 lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis"
   by (metis ex_in_conv nonempty_Basis someI_ex)
 
+lemma norm_some_Basis [simp]: "norm (SOME i. i \<in> Basis) = 1"
+  by (simp add: SOME_Basis)
+
 lemma (in euclidean_space) inner_sum_left_Basis[simp]:
     "b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b"
   by (simp add: inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.If_cases)