let R be Field; :: thesis: for E being FieldExtension of R
for T being Subset of E holds
( FAdj (R,T) == R iff T is Subset of R )
let S be FieldExtension of R; :: thesis: for T being Subset of S holds
( FAdj (R,T) == R iff T is Subset of R )
let T be Subset of S; :: thesis: ( FAdj (R,T) == R iff T is Subset of R )
set P = FAdj (R,T);
X: R is Subring of S by FIELD_4:def 1;
X1: ( R is Subfield of R & R is Subfield of S ) by FIELD_4:7, FIELD_4:1;
X2: carrierFA T = { x where x is Element of S : for U being Subfield of S st R is Subfield of U & T is Subset of U holds
x in U } by FIELD_6:def 5;

Z: 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 by X2;
hence o in the carrier of (FAdj (R,T)) by FIELD_6:def 6; :: thesis: verum

end;

now :: thesis: ( T is Subset of R implies FAdj (R,T) == R )

assume B0: T is Subset of R ; :: thesis: FAdj (R,T) == R

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

let o be object ; :: thesis: ( o in the carrier of (FAdj (R,T)) implies o in the carrier of R )
assume o in the carrier of (FAdj (R,T)) ; :: thesis: o in the carrier of R
then o in carrierFA T by FIELD_6:def 6;
then consider x being Element of S such that
B1: ( x = o & ( for U being Subfield of S st R is Subfield of U & T is Subset of U holds
x in U ) ) by X2;
x in R by X1, B0, B1;
hence o in the carrier of R by B1; :: thesis: verum

end;

then B1: the carrier of R = the carrier of (FAdj (R,T)) by Z, TARSKI:2;
B2: 1. (FAdj (R,T)) = 1. S by FIELD_6:def 6
.= 1. R by X, C0SP1:def 3 ;
B3: 0. (FAdj (R,T)) = 0. S by FIELD_6:def 6
.= 0. R by X, C0SP1:def 3 ;
B4: the addF of (FAdj (R,T)) = the addF of S || (carrierFA T) by FIELD_6:def 6
.= the addF of S || the carrier of R by B1, FIELD_6:def 6
.= the addF of R || the carrier of R by X, C0SP1:def 3 ;
the multF of (FAdj (R,T)) = the multF of S || (carrierFA T) by FIELD_6:def 6
.= the multF of S || the carrier of R by B1, FIELD_6:def 6
.= the multF of R || the carrier of R by X, C0SP1:def 3 ;
hence FAdj (R,T) == R by B5, B2, B3, B4, Z, TARSKI:2; :: thesis: verum

end;

hence ( FAdj (R,T) == R iff T is Subset of R ) by FIELD_6:35; :: thesis: verum