for x being Element of RAT+ holds x *' one = x