let n be Nat; 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; 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; 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; ( (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; for k being Nat st k <= n holds
F . (k + 1) = (n choose k) * ((p `^ k) *' (q `^ (n -' k)))
let k be Nat; ( k <= n implies F . (k + 1) = (n choose k) * ((p `^ k) *' (q `^ (n -' k))) )
assume A3:
k <= n
; 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
;
verum