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
RAdj (R,{a}) = 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
RAdj (R,{a}) = 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
RAdj (R,{a}) = RAdj (R,{b})
let a be Element of S; :: thesis: for b being Element of T st b = a holds
RAdj (R,{a}) = RAdj (R,{b})
let b be Element of T; :: thesis: ( b = a implies RAdj (R,{a}) = RAdj (R,{b}) )
assume AS: b = a ; :: thesis: RAdj (R,{a}) = RAdj (R,{b})
S is Subring of T by FIELD_4:def 1;
then RAdj (R,{a}) is Subring of T by ALGNUM_1:1;
hence RAdj (R,{a}) = RAdj (R,{b}) by AS, bb0, FIELD_6:14; :: thesis: verum