[STATEMENT]
lemma (in cring) finsum_reindex_bij_betw:
  assumes "bij_betw h S T" "g \<in> T \<rightarrow> carrier R"
  shows   "finsum R (\<lambda>x. g (h x)) S = finsum R g T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>x\<in>S. g (h x)) = finsum R g T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij_betw h S T
g \<in> T \<rightarrow> carrier R

goal (1 subgoal):
 1. (\<Oplus>x\<in>S. g (h x)) = finsum R g T
[PROOF STEP]
by (auto simp: bij_betw_def finsum_reindex)