let F be Field; :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for T1 being Subset of K
for T2 being finite Subset of K st T1 c= T2 & E == FAdj (F,T1) holds
FAdj (E,T2) = FAdj (F,T2)
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F
for T1 being Subset of K
for T2 being finite Subset of K st T1 c= T2 & E == FAdj (F,T1) holds
FAdj (E,T2) = FAdj (F,T2)
let K be E -extending FieldExtension of F; :: thesis: for T1 being Subset of K
for T2 being finite Subset of K st T1 c= T2 & E == FAdj (F,T1) holds
FAdj (E,T2) = FAdj (F,T2)
let T1 be Subset of K; :: thesis: for T2 being finite Subset of K st T1 c= T2 & E == FAdj (F,T1) holds
FAdj (E,T2) = FAdj (F,T2)
let T2 be finite Subset of K; :: thesis: ( T1 c= T2 & E == FAdj (F,T1) implies FAdj (E,T2) = FAdj (F,T2) )
assume AS: ( T1 c= T2 & E == FAdj (F,T1) ) ; :: thesis: FAdj (E,T2) = FAdj (F,T2)
then reconsider T1 = T1 as finite Subset of K ;
reconsider K1 = K as FieldExtension of FAdj (F,T1) by FIELD_4:7;
reconsider T3 = T2 as Subset of K1 ;
FAdj (E,T2) = FAdj ((FAdj (F,T1)),T3) by AS, lemNor3xx
.= FAdj (F,(T1 \/ T2)) by ug1 ;
hence FAdj (E,T2) = FAdj (F,T2) by AS, XBOOLE_1:12; :: thesis: verum