theorem Th24: :: BINOM:24

for R being non empty unital right_zeroed doubleLoopStr
for a, b being Element of R
for n being Nat holds ((a,b) In_Power n) . (n + 1) = b |^ n