∀[x,y:ℝ].  (rsin(x + y) = ((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))){ Auto }1. x : ℝ2. y : ℝ⊢ rsin(x + y) = ((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))