theorem :: ALGNUM_1:35

for x being Element of F_Complex holds F_Complex is Polynom-Ring F_Rat -homomorphic