theorem :: TOPREALC:9

for f, g being complex-valued Function holds (f - g) ^2 = (g - f) ^2