for k being positive Real
for X being non empty set holds (X --> 0) to_power k = X --> 0