theorem Th23: :: BINOM:23

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) . 1 = a |^ n