let F be Field; :: thesis: for E being FieldExtension of F
for T being Subset of E holds
( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field )
let E be FieldExtension of F; :: thesis: for T being Subset of E holds
( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field )
let T be Subset of E; :: thesis: ( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field )
set Pf = FAdj (F,T);
set Pr = RAdj (F,T);

now :: thesis: ( RAdj (F,T) is Field implies FAdj (F,T) = RAdj (F,T) )

assume RAdj (F,T) is Field ; :: thesis: FAdj (F,T) = RAdj (F,T)
then reconsider Prf = RAdj (F,T) as Field ;
F is Subring of Prf by RAsub;
then A: F is Subfield of Prf by FIELD_5:13;
B: Prf is Subfield of E by FIELD_5:13;
T is Subset of Prf by RAt;
then FAdj (F,T) is Subfield of Prf by A, B, FAsub2;
then C: FAdj (F,T) is Subring of Prf by FIELD_5:12;
RAdj (F,T) is Subring of FAdj (F,T) by RF;
hence FAdj (F,T) = RAdj (F,T) by C, RE; :: thesis: verum

end;

hence ( RAdj (F,T) = FAdj (F,T) iff RAdj (F,T) is Field ) ; :: thesis: verum