theorem Th25: :: WSIERP_1:25

for a, d being Nat st ex q being Rational st a = q |^ d holds
ex b being Nat st a = b |^ d