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

proof

now :: thesis: for o being object st o in T1 \/ T2 holds
o in the carrier of (FAdj ((FAdj (F,T2)),T3))

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

per cases then ( o in T1 or o in T2 ) by XBOOLE_0:def 3;

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

T1 is Subset of (FAdj ((FAdj (F,T2)),T3)) by AS, FIELD_6:35;
hence o in the carrier of (FAdj ((FAdj (F,T2)),T3)) by B1; :: thesis: verum

end;

suppose B1: o in T2 ; :: thesis: b₁ in the carrier of (FAdj ((FAdj (F,T2)),T3))

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

end;

end;

end;

hence T1 \/ T2 c= the carrier of (FAdj ((FAdj (F,T2)),T3)) ; :: thesis: verum

end;

then A: FAdj (F,(T1 \/ T2)) is Subfield of FAdj ((FAdj (F,T2)),T3) by AS, A1, FIELD_6:37;
A1: FAdj (F,T2) is Subfield of FAdj (F,(T1 \/ T2)) by FIELD_7:10, XBOOLE_1:7;
T2 \/ T3 is Subset of (FAdj (F,(T1 \/ T2))) by AS, FIELD_6:35;
then T3 c= the carrier of (FAdj (F,(T1 \/ T2))) by XBOOLE_1:11;
then FAdj ((FAdj (F,T2)),T3) is Subfield of FAdj (F,(T1 \/ T2)) by A1, AS, FIELD_6:37;
hence FAdj (F,(T1 \/ T2)) = FAdj ((FAdj (F,T2)),T3) by A, EC_PF_1:4; :: thesis: verum