let n be Nat; :: thesis: for a, b, c being Real holds Sum (((a + b),c) In_Power n) = Sum ((a,(b + c)) In_Power n)
let a, b, c be Real; :: thesis: Sum (((a + b),c) In_Power n) = Sum ((a,(b + c)) In_Power n)
Sum (((a + b),c) In_Power n) = ((a + b) + c) |^ n by NEWTON:30
.= (a + (b + c)) |^ n
.= Sum ((a,(b + c)) In_Power n) by NEWTON:30 ;
hence Sum (((a + b),c) In_Power n) = Sum ((a,(b + c)) In_Power n) ; :: thesis: verum