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