theorem :: NUMBER15:89

for a, x, y being Complex holds
( (x |^ 1) - (y |^ 1) = a iff x = a + y ) ;