theorem ug: :: FIELD_13:31

for R being Ring
for S being RingExtension of R
for T1, T2 being Subset of S
for S1 being RingExtension of RAdj (R,T2)
for T3 being Subset of S1 st S1 = S & T1 = T3 holds
RAdj (R,(T1 \/ T2)) = RAdj ((RAdj (R,T2)),T3)