let R be Field; :: thesis: for E being FieldExtension of R
for K being R -extending FieldExtension of R
for a being Element of E
for b being Element of K st b = a holds
the carrier of (RAdj (R,{a})) = the carrier of (RAdj (R,{b}))
let S be FieldExtension of R; :: thesis: for K being R -extending FieldExtension of R
for a being Element of S
for b being Element of K st b = a holds
the carrier of (RAdj (R,{a})) = the carrier of (RAdj (R,{b}))
let T be R -extending FieldExtension of R; :: thesis: for a being Element of S
for b being Element of T st b = a holds
the carrier of (RAdj (R,{a})) = the carrier of (RAdj (R,{b}))
let a be Element of S; :: thesis: for b being Element of T st b = a holds
the carrier of (RAdj (R,{a})) = the carrier of (RAdj (R,{b}))
let b be Element of T; :: thesis: ( b = a implies the carrier of (RAdj (R,{a})) = the carrier of (RAdj (R,{b})) )
assume AS: b = a ; :: thesis: the carrier of (RAdj (R,{a})) = the carrier of (RAdj (R,{b}))
A: the carrier of (RAdj (R,{a})) = { (Ext_eval (p,a)) where p is Polynomial of R : verum } by FIELD_6:45;
B: the carrier of (RAdj (R,{b})) = { (Ext_eval (p,b)) where p is Polynomial of R : verum } by FIELD_6:45;

C: now :: thesis: for o being object st o in the carrier of (RAdj (R,{a})) holds
o in the carrier of (RAdj (R,{b}))

let o be object ; :: thesis: ( o in the carrier of (RAdj (R,{a})) implies o in the carrier of (RAdj (R,{b})) )
assume o in the carrier of (RAdj (R,{a})) ; :: thesis: o in the carrier of (RAdj (R,{b}))
then consider p being Polynomial of R such that
D1: o = Ext_eval (p,a) by A;
p is Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
then o = Ext_eval (p,b) by D1, AS, FIELD_7:14;
hence o in the carrier of (RAdj (R,{b})) by B; :: thesis: verum

end;

now :: thesis: for o being object st o in the carrier of (RAdj (R,{b})) holds
o in the carrier of (RAdj (R,{a}))

let o be object ; :: thesis: ( o in the carrier of (RAdj (R,{b})) implies o in the carrier of (RAdj (R,{a})) )
assume o in the carrier of (RAdj (R,{b})) ; :: thesis: o in the carrier of (RAdj (R,{a}))
then consider p being Polynomial of R such that
D1: o = Ext_eval (p,b) by B;
p is Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
then o = Ext_eval (p,a) by D1, AS, FIELD_7:14;
hence o in the carrier of (RAdj (R,{a})) by A; :: thesis: verum

end;

hence the carrier of (RAdj (R,{a})) = the carrier of (RAdj (R,{b})) by C, TARSKI:2; :: thesis: verum