let F be Ring; :: thesis: for S being RingExtension of F
for T1, T2 being Subset of S
for S1 being RingExtension of RAdj (F,T2)
for T3 being Subset of S1 st S1 = S & T1 = T3 holds
RAdj (F,(T1 \/ T2)) = RAdj ((RAdj (F,T2)),T3)
let E be RingExtension of F; :: thesis: for T1, T2 being Subset of E
for S1 being RingExtension of RAdj (F,T2)
for T3 being Subset of S1 st S1 = E & T1 = T3 holds
RAdj (F,(T1 \/ T2)) = RAdj ((RAdj (F,T2)),T3)
let T1, T2 be Subset of E; :: thesis: for S1 being RingExtension of RAdj (F,T2)
for T3 being Subset of S1 st S1 = E & T1 = T3 holds
RAdj (F,(T1 \/ T2)) = RAdj ((RAdj (F,T2)),T3)
let E1 be RingExtension of RAdj (F,T2); :: thesis: for T3 being Subset of E1 st E1 = E & T1 = T3 holds
RAdj (F,(T1 \/ T2)) = RAdj ((RAdj (F,T2)),T3)
let T3 be Subset of E1; :: thesis: ( E1 = E & T1 = T3 implies RAdj (F,(T1 \/ T2)) = RAdj ((RAdj (F,T2)),T3) )
assume AS: ( E1 = E & T1 = T3 ) ; :: thesis: RAdj (F,(T1 \/ T2)) = RAdj ((RAdj (F,T2)),T3)
A1: F is Subring of RAdj ((RAdj (F,T2)),T3) by FIELD_4:def 1;
T1 \/ T2 c= the carrier of (RAdj ((RAdj (F,T2)),T3))

proof

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

let o be object ; :: thesis: ( o in T1 \/ T2 implies b₁ in the carrier of (RAdj ((RAdj (F,T2)),T3)) )
assume o in T1 \/ T2 ; :: thesis: b₁ in the carrier of (RAdj ((RAdj (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 (RAdj ((RAdj (F,T2)),T3))

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

end;

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

B2: T2 is Subset of (RAdj (F,T2)) by FIELD_6:30;
RAdj (F,T2) is Subring of RAdj ((RAdj (F,T2)),T3) by FIELD_6:31;
then the carrier of (RAdj (F,T2)) c= the carrier of (RAdj ((RAdj (F,T2)),T3)) by C0SP1:def 3;
hence o in the carrier of (RAdj ((RAdj (F,T2)),T3)) by B2, B1; :: thesis: verum

end;

end;

end;

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

end;

then A: RAdj (F,(T1 \/ T2)) is Subring of RAdj ((RAdj (F,T2)),T3) by AS, A1, FIELD_6:32;
A1: RAdj (F,T2) is Subring of RAdj (F,(T1 \/ T2)) by ext0, XBOOLE_1:7;
T2 \/ T3 is Subset of (RAdj (F,(T1 \/ T2))) by AS, FIELD_6:30;
then T3 c= the carrier of (RAdj (F,(T1 \/ T2))) by XBOOLE_1:11;
then RAdj ((RAdj (F,T2)),T3) is Subring of RAdj (F,(T1 \/ T2)) by A1, AS, FIELD_6:32;
hence RAdj (F,(T1 \/ T2)) = RAdj ((RAdj (F,T2)),T3) by A, FIELD_6:12; :: thesis: verum