let n be Nat; :: thesis: for R being commutative Ring
for p, q being Polynomial of R ex F being FinSequence of (Polynom-Ring R) st
( (p + q) `^ n = Sum F & len F = n + 1 & ( for k being Nat st k <= n holds
F . (k + 1) = (n choose k) * (@ ((p `^ k) *' (q `^ (n -' k)))) ) )
let R be commutative Ring; :: thesis: for p, q being Polynomial of R ex F being FinSequence of (Polynom-Ring R) st
( (p + q) `^ n = Sum F & len F = n + 1 & ( for k being Nat st k <= n holds
F . (k + 1) = (n choose k) * (@ ((p `^ k) *' (q `^ (n -' k)))) ) )
let p, q be Polynomial of R; :: thesis: ex F being FinSequence of (Polynom-Ring R) st
( (p + q) `^ n = Sum F & len F = n + 1 & ( for k being Nat st k <= n holds
F . (k + 1) = (n choose k) * (@ ((p `^ k) *' (q `^ (n -' k)))) ) )
A1: n in NAT by ORDINAL1:def 12;
take F = ((@ q),(@ p)) In_Power n; :: thesis: ( (p + q) `^ n = Sum F & len F = n + 1 & ( for k being Nat st k <= n holds
F . (k + 1) = (n choose k) * (@ ((p `^ k) *' (q `^ (n -' k)))) ) )
(p + q) `^ n = ((@ p) + (@ q)) |^ n by POLYNOM3:def 10;
hence A2: ( (p + q) `^ n = Sum F & len F = n + 1 ) by A1, BINOM:25, BINOM:def 7; :: thesis: for k being Nat st k <= n holds
F . (k + 1) = (n choose k) * (@ ((p `^ k) *' (q `^ (n -' k))))
let k be Nat; :: thesis: ( k <= n implies F . (k + 1) = (n choose k) * (@ ((p `^ k) *' (q `^ (n -' k)))) )
assume A3: k <= n ; :: thesis: F . (k + 1) = (n choose k) * (@ ((p `^ k) *' (q `^ (n -' k))))
set k1 = k + 1;
( 1 <= k + 1 & k + 1 <= len F ) by A2, A3, NAT_1:11, XREAL_1:6;
then A4: k + 1 in dom F by FINSEQ_3:25;
then A5: F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;
A6: (k + 1) - 1 = k ;
A7: ((@ q) |^ (n -' k)) * ((@ p) |^ k) = @ ((p `^ k) *' (q `^ (n -' k))) by POLYNOM3:def 10;
n -' k = n - k by A3, XREAL_1:233;
hence F . (k + 1) = ((n choose k) * ((@ q) |^ (n -' k))) * ((@ p) |^ k) by A4, A6, A5, BINOM:def 7
.= (n choose k) * (@ ((p `^ k) *' (q `^ (n -' k)))) by A7, BINOM:19 ;
:: thesis: verum