let a, b be Real; :: thesis: for n being Nat holds (a |^ (n + 1)) - (b |^ (n + 1)) = (a - b) * (Sum ((a,b) Subnomial n))
let n be Nat; :: thesis: (a |^ (n + 1)) - (b |^ (n + 1)) = (a - b) * (Sum ((a,b) Subnomial n))
A1: Sum ((a,b) Subnomial (n + 1)) = Sum ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) by RS
.= (Sum (a * ((a,b) Subnomial n))) + (b |^ (n + 1)) by RVSUM_2:31
.= (a * (Sum ((a,b) Subnomial n))) + (b |^ (n + 1)) by RVSUM_2:38 ;
Sum ((a,b) Subnomial (n + 1)) = Sum (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) by LS
.= (a |^ (n + 1)) + (Sum (b * ((a,b) Subnomial n))) by RVSUM_2:33
.= (b * (Sum ((a,b) Subnomial n))) + (a |^ (n + 1)) by RVSUM_2:38 ;
hence (a |^ (n + 1)) - (b |^ (n + 1)) = (a - b) * (Sum ((a,b) Subnomial n)) by A1; :: thesis: verum