[STATEMENT]
lemma sumj_upd_C: "sumj I i (s(C := x)) = sumj I i s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumj I i (s(C := x)) = sumj I i s
[PROOF STEP]
by (induct I) (auto simp add: sum_upd_C [unfolded fun_upd_def])