theorem :: NUMBER14:90

for x, y, z being Complex holds
( (((((x ^2) + (y ^2)) + (z ^2)) + x) + y) + z = 1 iff ((((2 * x) + 1) ^2) + (((2 * y) + 1) ^2)) + (((2 * z) + 1) ^2) = 7 ) ;