let a, b be Real; :: thesis: for n, i, l, m being Nat st i in dom ((a,b) Subnomial n) & m = i - 1 & l = n - m holds
((a,b) Subnomial n) . i = (a |^ l) * (b |^ m)
let n be Nat; :: thesis: for i, l, m being Nat st i in dom ((a,b) Subnomial n) & m = i - 1 & l = n - m holds
((a,b) Subnomial n) . i = (a |^ l) * (b |^ m)
let i, l, m be Nat; :: thesis: ( i in dom ((a,b) Subnomial n) & m = i - 1 & l = n - m implies ((a,b) Subnomial n) . i = (a |^ l) * (b |^ m) )
assume A1: ( i in dom ((a,b) Subnomial n) & m = i - 1 & l = n - m ) ; :: thesis: ((a,b) Subnomial n) . i = (a |^ l) * (b |^ m)
( dom (Newton_Coeff n) = dom ((a,b) Subnomial n) & dom (Newton_Coeff n) = dom ((a,b) In_Power n) ) by DOMN;
then A2: ( ((a,b) In_Power n) . i = ((n choose m) * (a |^ l)) * (b |^ m) & (Newton_Coeff n) . i = n choose m ) by A1, NEWTON:def 4, NEWTON:def 5;
((a,b) Subnomial n) . i = (((m + l) choose m) * ((a |^ l) * (b |^ m))) / ((m + l) choose m) by A1, A2, VALUED_1:17
.= (a |^ l) * (b |^ m) by XCMPLX_1:89 ;
hence ((a,b) Subnomial n) . i = (a |^ l) * (b |^ m) ; :: thesis: verum