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

proof

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

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

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

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

{b} is Subset of (FAdj ((FAdj (F,{b})),T1))

proof

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

let o be object ; :: thesis: ( o in {b} implies o in the carrier of (FAdj ((FAdj (F,{b})),T1)) )
assume B3: o in {b} ; :: thesis: o in the carrier of (FAdj ((FAdj (F,{b})),T1))
B4: {b} is Subset of (FAdj (F,{b})) by FIELD_6:35;
FAdj (F,{b}) is Subfield of FAdj ((FAdj (F,{b})),T1) by FIELD_6:36;
then the carrier of (FAdj (F,{b})) c= the carrier of (FAdj ((FAdj (F,{b})),T1)) by EC_PF_1:def 1;
hence o in the carrier of (FAdj ((FAdj (F,{b})),T1)) by B3, B4; :: thesis: verum

end;

hence {b} is Subset of (FAdj ((FAdj (F,{b})),T1)) by TARSKI:def 3; :: thesis: verum

end;

hence o in the carrier of (FAdj ((FAdj (F,{b})),T1)) by B1; :: thesis: verum

end;

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

T is Subset of (FAdj ((FAdj (F,{b})),T1)) by AS, FIELD_6:35;
hence o in the carrier of (FAdj ((FAdj (F,{b})),T1)) by B1; :: thesis: verum

end;

end;

end;

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

end;

then A: FAdj (F,({b} \/ T)) is Subfield of FAdj ((FAdj (F,{b})),T1) by AS, A1, FIELD_6:37;
A1: FAdj (F,{b}) 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 T1 c= the carrier of (FAdj (F,({b} \/ T))) by AS, XBOOLE_1:11;
then FAdj ((FAdj (F,{b})),T1) is Subfield of FAdj (F,({b} \/ T)) by A1, AS, FIELD_6:37;
hence FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,{b})),T1) by A, EC_PF_1:4; :: thesis: verum