let a, b be positive Real; :: thesis: for n being Real holds (a to_power (n + 1)) + (b to_power (n + 1)) = ((((a to_power n) + (b to_power n)) * (a + b)) + ((a - b) * ((a to_power n) - (b to_power n)))) / 2
let n be Real; :: thesis: (a to_power (n + 1)) + (b to_power (n + 1)) = ((((a to_power n) + (b to_power n)) * (a + b)) + ((a - b) * ((a to_power n) - (b to_power n)))) / 2
( a to_power 1 = a & b to_power 1 = b ) ;
hence (a to_power (n + 1)) + (b to_power (n + 1)) = ((((a to_power n) + (b to_power n)) * (a + b)) + ((a - b) * ((a to_power n) - (b to_power n)))) / 2 by N158; :: thesis: verum