theorem Th8: :: LPSPACE2:8

for X being non empty set
for f being PartFunc of X,REAL holds f to_power 1 = f