theorem Th22: :: BINOM:22

for R being non empty unital right_zeroed doubleLoopStr
for a, b being Element of R holds (a,b) In_Power 0 = <*(1_ R)*>