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