let x be Element of F_Complex; :: thesis: F_Complex is Polynom-Ring F_Rat -homomorphic
hom_Ext_eval (x,F_Rat) is RingHomomorphism ;
hence F_Complex is Polynom-Ring F_Rat -homomorphic ; :: thesis: verum