[STATEMENT]
lemma smult_mult2: fixes a :: "'a::comm_ring_1" shows "a *\<^sub>S (A * B) = A * (a *\<^sub>S B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a *\<^sub>S (A * B) = A * a *\<^sub>S B
[PROOF STEP]
by transfer (simp add: sum_distrib_left field_simps)