theorem :: BINOM:25

for R being non empty add-cancelable left_zeroed distributive unital associative commutative Abelian add-associative right_zeroed doubleLoopStr
for a, b being Element of R
for n being Element of NAT holds (a + b) |^ n = Sum ((a,b) In_Power n)