for a, b, i, m, n being Nat st 1 <= i & i <= (len ((a,b) In_Power n)) - m holds
a |^ m divides ((a,b) In_Power n) . i