for x1, y1 being Element of F_Complex
for x2, y2 being Complex st x1 = x2 & y1 = y2 holds
x1 - y1 = x2 - y2