let F be Field; :: thesis: for E, K being FieldExtension of F
for U1 being FieldExtension of E
for U2 being FieldExtension of K
for T1 being Subset of U1
for T2 being Subset of U2 st U1 = U2 & T1 = T2 & E == K holds
FAdj (E,T1) = FAdj (K,T2)
let E, K be FieldExtension of F; :: thesis: for U1 being FieldExtension of E
for U2 being FieldExtension of K
for T1 being Subset of U1
for T2 being Subset of U2 st U1 = U2 & T1 = T2 & E == K holds
FAdj (E,T1) = FAdj (K,T2)
let U1 be FieldExtension of E; :: thesis: for U2 being FieldExtension of K
for T1 being Subset of U1
for T2 being Subset of U2 st U1 = U2 & T1 = T2 & E == K holds
FAdj (E,T1) = FAdj (K,T2)
let U2 be FieldExtension of K; :: thesis: for T1 being Subset of U1
for T2 being Subset of U2 st U1 = U2 & T1 = T2 & E == K holds
FAdj (E,T1) = FAdj (K,T2)
let T1 be Subset of U1; :: thesis: for T2 being Subset of U2 st U1 = U2 & T1 = T2 & E == K holds
FAdj (E,T1) = FAdj (K,T2)
let T2 be Subset of U2; :: thesis: ( U1 = U2 & T1 = T2 & E == K implies FAdj (E,T1) = FAdj (K,T2) )
assume AS: ( U1 = U2 & T1 = T2 & E == K ) ; :: thesis: FAdj (E,T1) = FAdj (K,T2)
A: FAdj (E,T1) is Subfield of FAdj (K,T2)

proof

FAdj (K,T2) is FieldExtension of E by AS, FIELD_12:37;
then A1: E is Subfield of FAdj (K,T2) by FIELD_4:7;
T1 is Subset of (FAdj (K,T2)) by AS, FIELD_6:35;
hence FAdj (E,T1) is Subfield of FAdj (K,T2) by AS, A1, FIELD_6:37; :: thesis: verum

end;

FAdj (K,T2) is Subfield of FAdj (E,T1)

proof

FAdj (E,T1) is FieldExtension of K by AS, FIELD_12:37;
then A1: K is Subfield of FAdj (E,T1) by FIELD_4:7;
T2 is Subset of (FAdj (E,T1)) by AS, FIELD_6:35;
hence FAdj (K,T2) is Subfield of FAdj (E,T1) by AS, A1, FIELD_6:37; :: thesis: verum

end;

hence FAdj (E,T1) = FAdj (K,T2) by A, EC_PF_1:4; :: thesis: verum