[mizar] properties

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

In mathematics there are unary operations (let say f) satisfying property

f^m(x) = f^n(x).

Some of them have commonly used names, like

for m = 2, n = 1, that is f(f(x)) = f(x) - projectivity

for m = 2, n = 0, that is f(f(x)) = x - involutiveness



In the MML there are theorems about operations satisfying the property
for m = 1 and n = 0, for example:

theorem
  for m being Nat holds m = abs m

theorem
 for T being non empty TopSpace, a being Point of T,
     P being constant Path of a,a
 holds - P = P

We are thinking about implementation of the property (m=1,n=0) in Mizar, 
and we are looking for an appropriate name for it.

Any suggestions?

Best regards
Artur