let n be Nat; :: thesis: for R being commutative Ring
for p, q being Polynomial of R ex F being FinSequence of () 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 () 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 () 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 ; :: 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 ;
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 ;
hence F . (k + 1) = ((n choose k) * ((@ q) |^ (n -' k))) * ((@ p) |^ k) by
.= (n choose k) * ((p `^ k) *' (q `^ (n -' k))) by ;
:: thesis: verum