for x being Element of F_Complex
for a being Element of F_Rat holds a in FQ x