let k, n be Element of NAT ; for x, y being real number st k <= n holds
(x,y In_Power n) . (k + 1) = ((n choose k) * (x ^ (n - k))) * (y ^ k)
let x, y be real number ; ( 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 ;
A1:
( k + 1 >= 0 + 1 & len (x,y In_Power n) = n + 1 )
by NEWTON:def 4, XREAL_1:8;
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:18;
k + 1 <= n + 1
by A2, XREAL_1:8;
then
k + 1 in dom (x,y In_Power n)
by A1, FINSEQ_3:27;
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