let m, n be Nat; :: thesis: for a1, b1 being Complex holds ((((a1 |^ m) + (b1 |^ m)) * ((a1 |^ n) + (b1 |^ n))) + (((a1 |^ n) - (b1 |^ n)) * ((a1 |^ m) - (b1 |^ m)))) / 2 = (a1 |^ (m + n)) + (b1 |^ (m + n))
let a1, b1 be Complex; :: thesis: ((((a1 |^ m) + (b1 |^ m)) * ((a1 |^ n) + (b1 |^ n))) + (((a1 |^ n) - (b1 |^ n)) * ((a1 |^ m) - (b1 |^ m)))) / 2 = (a1 |^ (m + n)) + (b1 |^ (m + n))
thus ((((a1 |^ m) + (b1 |^ m)) * ((a1 |^ n) + (b1 |^ n))) + (((a1 |^ n) - (b1 |^ n)) * ((a1 |^ m) - (b1 |^ m)))) / 2 = (((((a1 |^ m) * (a1 |^ n)) + ((b1 |^ m) * (b1 |^ n))) + ((a1 |^ n) * (a1 |^ m))) + ((b1 |^ n) * (b1 |^ m))) / 2
.= ((((a1 |^ (m + n)) + ((b1 |^ m) * (b1 |^ n))) + ((a1 |^ n) * (a1 |^ m))) + ((b1 |^ n) * (b1 |^ m))) / 2 by NEWTON:8
.= ((((a1 |^ (m + n)) + (b1 |^ (m + n))) + ((a1 |^ n) * (a1 |^ m))) + ((b1 |^ n) * (b1 |^ m))) / 2 by NEWTON:8
.= ((((a1 |^ (m + n)) + (b1 |^ (m + n))) + (a1 |^ (m + n))) + ((b1 |^ n) * (b1 |^ m))) / 2 by NEWTON:8
.= ((((a1 |^ (m + n)) + (b1 |^ (m + n))) + (a1 |^ (n + m))) + (b1 |^ (n + m))) / 2 by NEWTON:8
.= (a1 |^ (m + n)) + (b1 |^ (m + n)) ; :: thesis: verum