let F be Field; :: thesis: for E being Polynom-Ring F -homomorphic FieldExtension of F
for a being Element of E holds the carrier of (RAdj (F,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }
let E be Polynom-Ring F -homomorphic FieldExtension of F; :: thesis: for a being Element of E holds the carrier of (RAdj (F,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }
let a be Element of E; :: thesis: the carrier of (RAdj (F,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }
thus the carrier of (RAdj (F,{a})) = the carrier of (Image (hom_Ext_eval (a,F))) by lemphi4
.= rng (hom_Ext_eval (a,F)) by RING_2:def 6
.= { (Ext_eval (p,a)) where p is Polynomial of F : verum } by lemphi1 ; :: thesis: verum