diff -r 2d3df8633dad -r db890d9fc5c2 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -75,6 +75,10 @@
   "(\<Sum>i\<in>Basis. f i *\<^sub>R i) = b \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
   by (subst euclidean_eq_iff) simp
 
+lemma (in euclidean_space) euclidean_representation_setsum':
+  "b = (\<Sum>i\<in>Basis. f i *\<^sub>R i) \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
+  by (auto simp add: euclidean_representation_setsum[symmetric])
+
 lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
   unfolding euclidean_representation_setsum by simp