let x be Element of F_Complex; :: thesis: for a being Element of F_Rat holds a in FQ x
let a be Element of F_Rat; :: thesis: a in FQ x
reconsider f = <%a%> as Polynomial of F_Rat ;
A2: dom (hom_Ext_eval (x,F_Rat)) = the carrier of (Polynom-Ring F_Rat) by FUNCT_2:def 1;
A3: Ext_eval (f,x) = In (a,F_Complex) by Th3, Th25;
reconsider f = f as Element of (Polynom-Ring F_Rat) by POLYNOM3:def 10;
In (a,F_Complex) = (hom_Ext_eval (x,F_Rat)) . f by A3, Def9;
hence a in FQ x by A2, FUNCT_1:def 3; :: thesis: verum