let R be Field; :: thesis: for E being FieldExtension of R
for T being Subset of E
for U being Subfield of E st R is Subfield of U & T is Subset of U holds
FAdj (R,T) is Subfield of U
let S be FieldExtension of R; :: thesis: for T being Subset of S
for U being Subfield of S st R is Subfield of U & T is Subset of U holds
FAdj (R,T) is Subfield of U
let T be Subset of S; :: thesis: for U being Subfield of S st R is Subfield of U & T is Subset of U holds
FAdj (R,T) is Subfield of U
let U be Subfield of S; :: thesis: ( R is Subfield of U & T is Subset of U implies FAdj (R,T) is Subfield of U )
assume AS: ( R is Subfield of U & T is Subset of U ) ; :: thesis: FAdj (R,T) is Subfield of U
set P = FAdj (R,T);
A: 1. (FAdj (R,T)) = 1. S by dFA
.= 1. U by EC_PF_1:def 1 ;
B: 0. (FAdj (R,T)) = 0. S by dFA
.= 0. U by EC_PF_1:def 1 ;
C: the carrier of (FAdj (R,T)) c= the carrier of U
proof
now :: thesis: for o being object st o in the carrier of (FAdj (R,T)) holds
o in the carrier of U
let o be object ; :: thesis: ( o in the carrier of (FAdj (R,T)) implies o in the carrier of U )
assume o in the carrier of (FAdj (R,T)) ; :: thesis: o in the carrier of U
then o in carrierFA T by dFA;
then consider x being Element of S such that
C2: ( x = o & ( for U being Subfield of S st R is Subfield of U & T is Subset of U holds
x in U ) ) ;
x in U by C2, AS;
hence o in the carrier of U by C2; :: thesis: verum
end;
hence the carrier of (FAdj (R,T)) c= the carrier of U ; :: thesis: verum
end;
then Y: [: the carrier of (FAdj (R,T)), the carrier of (FAdj (R,T)):] c= [: the carrier of U, the carrier of U:] by ZFMISC_1:96;
D: the addF of U || the carrier of (FAdj (R,T)) = ( the addF of S || the carrier of U) || the carrier of (FAdj (R,T)) by EC_PF_1:def 1
.= the addF of S || the carrier of (FAdj (R,T)) by Y, FUNCT_1:51
.= the addF of S || (carrierFA T) by dFA
.= the addF of (FAdj (R,T)) by dFA ;
the multF of U || the carrier of (FAdj (R,T)) = ( the multF of S || the carrier of U) || the carrier of (FAdj (R,T)) by EC_PF_1:def 1
.= the multF of S || the carrier of (FAdj (R,T)) by Y, FUNCT_1:51
.= the multF of S || (carrierFA T) by dFA
.= the multF of (FAdj (R,T)) by dFA ;
hence FAdj (R,T) is Subfield of U by A, B, C, D, EC_PF_1:def 1; :: thesis: verum