let R be Field; :: thesis: for E being FieldExtension of R
for T being Subset of E holds R is Subfield of FAdj (R,T)
let S be FieldExtension of R; :: thesis: for T being Subset of S holds R is Subfield of FAdj (R,T)
let T be Subset of S; :: thesis: R is Subfield of FAdj (R,T)
set P = FAdj (R,T);
X: R is Subring of S by FIELD_4:def 1;
A: 1. (FAdj (R,T)) = 1. S by dFA
.= 1. R by X, C0SP1:def 3 ;
B: 0. (FAdj (R,T)) = 0. S by dFA
.= 0. R by X, C0SP1:def 3 ;
C: the carrier of R c= the carrier of (FAdj (R,T))

proof

now :: thesis: for o being object st o in the carrier of R holds
o in the carrier of (FAdj (R,T))

let o be object ; :: thesis: ( o in the carrier of R implies o in the carrier of (FAdj (R,T)) )
assume C1: o in the carrier of R ; :: thesis: o in the carrier of (FAdj (R,T))
the carrier of R c= the carrier of S by X, C0SP1:def 3;
then reconsider a = o as Element of S by C1;

now :: thesis: for U being Subfield of S st R is Subfield of U & T is Subset of U holds
o in U

let U be Subfield of S; :: thesis: ( R is Subfield of U & T is Subset of U implies o in U )
assume ( R is Subfield of U & T is Subset of U ) ; :: thesis: o in U
then the carrier of R c= the carrier of U by EC_PF_1:def 1;
hence o in U by C1; :: thesis: verum

end;

then a in carrierFA T ;
hence o in the carrier of (FAdj (R,T)) by dFA; :: thesis: verum

end;

hence the carrier of R c= the carrier of (FAdj (R,T)) ; :: thesis: verum

end;

then Y: [: the carrier of R, the carrier of R:] c= [: the carrier of (FAdj (R,T)), the carrier of (FAdj (R,T)):] by ZFMISC_1:96;
D: the addF of (FAdj (R,T)) || the carrier of R = ( the addF of S || (carrierFA T)) || the carrier of R by dFA
.= ( the addF of S || the carrier of (FAdj (R,T))) || the carrier of R by dFA
.= the addF of S || the carrier of R by Y, FUNCT_1:51
.= the addF of R by X, C0SP1:def 3 ;
the multF of (FAdj (R,T)) || the carrier of R = ( the multF of S || (carrierFA T)) || the carrier of R by dFA
.= ( the multF of S || the carrier of (FAdj (R,T))) || the carrier of R by dFA
.= the multF of S || the carrier of R by Y, FUNCT_1:51
.= the multF of R by X, C0SP1:def 3 ;
hence R is Subfield of FAdj (R,T) by A, B, C, D, EC_PF_1:def 1; :: thesis: verum