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

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