theorem Th19: :: IRRAT_1:19

for k, n being Nat
for x, y being Real st k <= n holds
((x,y) In_Power n) . (k + 1) = ((n choose k) * (x ^ (n - k))) * (y ^ k)