theorem TT2: :: FIELD_16:5

for L being non empty 1-sorted
for f being bijective Function of L,L
for n, m being Nat holds
( f `^ (n + 1) = f `^ (m + 1) iff f `^ n = f `^ m )