let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E holds FAdj (F,{a,(- a)}) = FAdj (F,{a})
let E be FieldExtension of F; :: thesis: for a being Element of E holds FAdj (F,{a,(- a)}) = FAdj (F,{a})
let a be Element of E; :: thesis: FAdj (F,{a,(- a)}) = FAdj (F,{a})
Y: FAdj (F,{a}) is Subfield of FAdj (F,{a,(- a)}) by FIELD_7:10, ZFMISC_1:7;

now :: thesis: for o being object st o in the carrier of (FAdj (F,{a,(- a)})) holds
o in the carrier of (FAdj (F,{a}))

let o be object ; :: thesis: ( o in the carrier of (FAdj (F,{a,(- a)})) implies o in the carrier of (FAdj (F,{a})) )
assume A: o in the carrier of (FAdj (F,{a,(- a)})) ; :: thesis: o in the carrier of (FAdj (F,{a}))
the carrier of (FAdj (F,{a,(- a)})) = carrierFA {a,(- a)} by FIELD_6:def 6
.= { x where x is Element of E : for U being Subfield of E st F is Subfield of U & {a,(- a)} is Subset of U holds
x in U } ;
then consider oe being Element of E such that
C: ( oe = o & ( for U being Subfield of E st F is Subfield of U & {a,(- a)} is Subset of U holds
oe in U ) ) by A;

D: now :: thesis: for U being Subfield of E st F is Subfield of U & {a} is Subset of U holds
oe in U

let U be Subfield of E; :: thesis: ( F is Subfield of U & {a} is Subset of U implies oe in U )
assume D: ( F is Subfield of U & {a} is Subset of U ) ; :: thesis: oe in U
E: a in {a} by TARSKI:def 1;
then reconsider au = a as Element of U by D;
U is Subring of E by FIELD_5:12;
then F: - au = - a by FIELD_6:17;

now :: thesis: for u being object st u in {a,(- a)} holds
u in the carrier of U

let u be object ; :: thesis: ( u in {a,(- a)} implies b₁ in the carrier of U )
assume u in {a,(- a)} ; :: thesis: b₁ in the carrier of U

per cases then ( u = a or u = - a ) by TARSKI:def 2;

suppose u = a ; :: thesis: b₁ in the carrier of U

hence u in the carrier of U by E, D; :: thesis: verum

end;

suppose u = - a ; :: thesis: b₁ in the carrier of U

hence u in the carrier of U by F; :: thesis: verum

end;

end;

end;

then {a,(- a)} is Subset of U by TARSKI:def 3;
hence oe in U by C, D; :: thesis: verum

end;

the carrier of (FAdj (F,{a})) = carrierFA {a} by FIELD_6:def 6
.= { x where x is Element of E : for U being Subfield of E st F is Subfield of U & {a} is Subset of U holds
x in U } ;
hence o in the carrier of (FAdj (F,{a})) by C, D; :: thesis: verum

end;

then the carrier of (FAdj (F,{a,(- a)})) c= the carrier of (FAdj (F,{a})) ;
then FAdj (F,{a,(- a)}) is Subfield of FAdj (F,{a}) by EC_PF_1:6;
hence FAdj (F,{a,(- a)}) = FAdj (F,{a}) by Y, EC_PF_1:4; :: thesis: verum