--- 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