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