for x being Element of F_Complex
for z, w being Element of FQ x holds (FQ_add x) . (z,w) = z + w