theorem Th73: :: PREPOWER:73

for a being Real holds 1 #R a = 1