let F be Field; :: thesis: for E being FieldExtension of F
for b being Element of E
for T being Subset of E
for E1 being FieldExtension of FAdj (F,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
let E be FieldExtension of F; :: thesis: for b being Element of E
for T being Subset of E
for E1 being FieldExtension of FAdj (F,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
let b be Element of E; :: thesis: for T being Subset of E
for E1 being FieldExtension of FAdj (F,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
let T be Subset of E; :: thesis: for E1 being FieldExtension of FAdj (F,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
let E1 be FieldExtension of FAdj (F,T); :: thesis: for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
let b1 be Element of E1; :: thesis: ( E1 = E & b1 = b implies FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1}) )
assume AS: ( E1 = E & b1 = b ) ; :: thesis: FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
A1: F is Subfield of FAdj ((FAdj (F,T)),{b1}) by FIELD_4:7;
{b} \/ T c= the carrier of (FAdj ((FAdj (F,T)),{b1}))

proof

now :: thesis: for o being object st o in {b} \/ T holds
o in the carrier of (FAdj ((FAdj (F,T)),{b1}))

let o be object ; :: thesis: ( o in {b} \/ T implies b₁ in the carrier of (FAdj ((FAdj (F,T)),{b1})) )
assume o in {b} \/ T ; :: thesis: b₁ in the carrier of (FAdj ((FAdj (F,T)),{b1}))

per cases then ( o in {b} or o in T ) by XBOOLE_0:def 3;

suppose o in {b} ; :: thesis: b₁ in the carrier of (FAdj ((FAdj (F,T)),{b1}))

then B1: o = b by TARSKI:def 1;
B2: {b1} is Subset of (FAdj ((FAdj (F,T)),{b1})) by FIELD_6:35;
b in {b1} by AS, TARSKI:def 1;
hence o in the carrier of (FAdj ((FAdj (F,T)),{b1})) by B1, B2; :: thesis: verum

end;

suppose B1: o in T ; :: thesis: b₁ in the carrier of (FAdj ((FAdj (F,T)),{b1}))

B2: T is Subset of (FAdj (F,T)) by FIELD_6:35;
FAdj (F,T) is Subfield of FAdj ((FAdj (F,T)),{b1}) by FIELD_6:36;
then the carrier of (FAdj (F,T)) c= the carrier of (FAdj ((FAdj (F,T)),{b1})) by EC_PF_1:def 1;
hence o in the carrier of (FAdj ((FAdj (F,T)),{b1})) by B2, B1; :: thesis: verum

end;

end;

end;

hence {b} \/ T c= the carrier of (FAdj ((FAdj (F,T)),{b1})) ; :: thesis: verum

end;

then A: FAdj (F,({b} \/ T)) is Subfield of FAdj ((FAdj (F,T)),{b1}) by AS, A1, FIELD_6:37;
A1: FAdj (F,T) is Subfield of FAdj (F,({b} \/ T)) by ext0, XBOOLE_1:7;
{b} \/ T is Subset of (FAdj (F,({b} \/ T))) by FIELD_6:35;
then {b1} c= the carrier of (FAdj (F,({b} \/ T))) by AS, XBOOLE_1:11;
then FAdj ((FAdj (F,T)),{b1}) is Subfield of FAdj (F,({b} \/ T)) by A1, AS, FIELD_6:37;
hence FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1}) by A, EC_PF_1:4; :: thesis: verum