for x being Element of F_Complex
for z, w being Element of FQ x holds (FQ_mult x) . (z,w) = z * w