let F be Field; :: thesis: for E being FieldExtension of F
for T being Subset of E
for a being Element of E st a in the carrier of (FAdj (F,T)) holds
FAdj (F,(T \/ {a})) = FAdj (F,T)
let E be FieldExtension of F; :: thesis: for T being Subset of E
for a being Element of E st a in the carrier of (FAdj (F,T)) holds
FAdj (F,(T \/ {a})) = FAdj (F,T)
let T be Subset of E; :: thesis: for a being Element of E st a in the carrier of (FAdj (F,T)) holds
FAdj (F,(T \/ {a})) = FAdj (F,T)
let a be Element of E; :: thesis: ( a in the carrier of (FAdj (F,T)) implies FAdj (F,(T \/ {a})) = FAdj (F,T) )
assume a in the carrier of (FAdj (F,T)) ; :: thesis: FAdj (F,(T \/ {a})) = FAdj (F,T)
then A: {a} c= the carrier of (FAdj (F,T)) by TARSKI:def 1;
reconsider E1 = E as FieldExtension of FAdj (F,T) by FIELD_4:7;
reconsider a1 = a as Element of E1 ;
FAdj (F,(T \/ {a})) = FAdj ((FAdj (F,T)),{a1}) by FIELD_7:34;
hence FAdj (F,(T \/ {a})) = FAdj (F,T) by A, FIELD_6:38; :: thesis: verum