let F be Field; :: thesis: for E being Polynom-Ring F -homomorphic FieldExtension of F
for a being Element of E holds RAdj (F,{a}) = Image (hom_Ext_eval (a,F))
let E be Polynom-Ring F -homomorphic FieldExtension of F; :: thesis: for a being Element of E holds RAdj (F,{a}) = Image (hom_Ext_eval (a,F))
let a be Element of E; :: thesis: RAdj (F,{a}) = Image (hom_Ext_eval (a,F))
A0: F is Subring of E by FIELD_4:def 1;
set R = Image (hom_Ext_eval (a,F));
set S = RAdj (F,{a});
set f = hom_Ext_eval (a,F);

now :: thesis: for o being object st o in {a} holds
o in the carrier of (Image (hom_Ext_eval (a,F)))

let o be object ; :: thesis: ( o in {a} implies o in the carrier of (Image (hom_Ext_eval (a,F))) )
assume o in {a} ; :: thesis: o in the carrier of (Image (hom_Ext_eval (a,F)))
then A1: o = a by TARSKI:def 1;
reconsider p = <%(0. F),(1. F)%> as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider q = p as Element of the carrier of (Polynom-Ring E) ;
A2: dom (hom_Ext_eval (a,F)) = the carrier of (Polynom-Ring F) by FUNCT_2:def 1;
( 0. E = 0. F & 1. E = 1. F ) by A0, C0SP1:def 3;
then A3: q = <%(0. E),(1. E)%> by A0, pr20;
(hom_Ext_eval (a,F)) . p = Ext_eval (p,a) by ALGNUM_1:def 11
.= eval (q,a) by FIELD_4:26
.= (0. E) + ((1. E) * a) by A3, POLYNOM5:44
.= a ;
then a in rng (hom_Ext_eval (a,F)) by A2, FUNCT_1:def 3;
hence o in the carrier of (Image (hom_Ext_eval (a,F))) by A1, RING_2:def 6; :: thesis: verum

end;

then A: {a} is Subset of the carrier of (Image (hom_Ext_eval (a,F))) by TARSKI:def 3;
F is Subring of Image (hom_Ext_eval (a,F)) by lemphi3;
then RAdj (F,{a}) is Subring of Image (hom_Ext_eval (a,F)) by A, RAsub2;
then the carrier of (RAdj (F,{a})) c= the carrier of (Image (hom_Ext_eval (a,F))) by C0SP1:def 3;
then V: the carrier of (RAdj (F,{a})) c= rng (hom_Ext_eval (a,F)) by RING_2:def 6;
rng (hom_Ext_eval (a,F)) c= the carrier of (RAdj (F,{a})) by lemphi2;
then the carrier of (RAdj (F,{a})) = rng (hom_Ext_eval (a,F)) by V, TARSKI:2
.= the carrier of (Image (hom_Ext_eval (a,F))) by RING_2:def 6 ;
hence RAdj (F,{a}) = Image (hom_Ext_eval (a,F)) by RE1; :: thesis: verum