let k, n be 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)
let x, y be Real; ( k <= n implies ((x,y) In_Power n) . (k + 1) = ((n choose k) * (x ^ (n - k))) * (y ^ k) )
reconsider i1 = (k + 1) - 1 as Element of NAT by ORDINAL1:def 12;
A1:
( k + 1 >= 0 + 1 & len ((x,y) In_Power n) = n + 1 )
by NEWTON:def 4, XREAL_1:6;
assume A2:
k <= n
; ((x,y) In_Power n) . (k + 1) = ((n choose k) * (x ^ (n - k))) * (y ^ k)
then reconsider l = n - i1 as Element of NAT by INT_1:5;
k + 1 <= n + 1
by A2, XREAL_1:6;
then
k + 1 in dom ((x,y) In_Power n)
by A1, FINSEQ_3:25;
hence ((x,y) In_Power n) . (k + 1) =
((n choose i1) * (x ^ l)) * (y |^ i1)
by NEWTON:def 4
.=
((n choose k) * (x ^ (n - k))) * (y ^ k)
;
verum