theorem ug1: :: FIELD_13:18

for F being Field
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)