for a, b, c being Ordinal st b <> 0 holds
a mod^ (exp (b,c)) in exp (b,c)