theorem ug: :: FIELD_7:34

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,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})