theorem ug1: :: FIELD_7:35

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