Re: [mizar] Functions between the positive real numbers?

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Dear Freek,

Few seconds after sending the letter I recognized that you need the set 
of all positive real numbers and the definitions that I mentioned deals 
with the set of all non negative real numbers. Sorry.

Stiil, I do not think that it is worth to introduce such functions.
The attributes are easier to manipulate.

Happy Eastern,
Andrzej