let a, b be Real; :: thesis: for n being Nat holds (a,b) In_Power n = (Newton_Coeff n) (#) ((a,b) Subnomial n)
let n be Nat; :: thesis: (a,b) In_Power n = (Newton_Coeff n) (#) ((a,b) Subnomial n)
A0a: dom ((a,b) In_Power n) = dom (Newton_Coeff n) by DOMN;
then A0: dom ((a,b) In_Power n) = (dom (Newton_Coeff n)) /\ (dom ((a,b) In_Power n)) ;
then A1: dom ((a,b) In_Power n) = dom ((a,b) Subnomial n) by VALUED_1:16;
for c being object st c in dom ((a,b) In_Power n) holds
((a,b) In_Power n) . c = ((Newton_Coeff n) . c) * (((a,b) Subnomial n) . c)

proof

let c be object ; :: thesis: ( c in dom ((a,b) In_Power n) implies ((a,b) In_Power n) . c = ((Newton_Coeff n) . c) * (((a,b) Subnomial n) . c) )
assume B1: c in dom ((a,b) In_Power n) ; :: thesis: ((a,b) In_Power n) . c = ((Newton_Coeff n) . c) * (((a,b) Subnomial n) . c)
reconsider c = c as positive Nat by B1, FINSEQ_3:25;
set m = c - 1;
c <= len (Newton_Coeff ((n + 1) - 1)) by B1, A0a, FINSEQ_3:25;
then consider k being Nat such that
B2: n + 1 = c + k by NAT_1:10;
B3: ( n = (c - 1) + k & k = n - (c - 1) ) by B2;
((Newton_Coeff ((c - 1) + k)) . ((c - 1) + 1)) * (((a,b) Subnomial ((c - 1) + k)) . ((c - 1) + 1)) = (((c - 1) + k) choose (c - 1)) * (((a,b) Subnomial ((c - 1) + k)) . ((c - 1) + 1)) by B2, B1, A0a, NEWTON:def 5
.= (((c - 1) + k) choose (c - 1)) * ((a |^ k) * (b |^ (c - 1))) by B1, A1, B3, Def2
.= ((((c - 1) + k) choose (c - 1)) * (a |^ k)) * (b |^ (c - 1))
.= ((a,b) In_Power ((c - 1) + k)) . ((c - 1) + 1) by NEWTON:def 4, B1, B3 ;
hence ((a,b) In_Power n) . c = ((Newton_Coeff n) . c) * (((a,b) Subnomial n) . c) by B2; :: thesis: verum

end;

hence (a,b) In_Power n = (Newton_Coeff n) (#) ((a,b) Subnomial n) by A0, A1, VALUED_1:def 4; :: thesis: verum