theorem Th1: :: SIN_COS7:1

for x being Real st x > 0 holds
1 / x = x to_power (- 1)