let k, n be Element of NAT ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ((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) ;
:: thesis: verum