for m, n being natural Ordinal st {} in m holds
n mod^ m in m