theorem bb1: :: FIELD_10:8

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for a being Element of E
for b being Element of K st b = a holds
RAdj (F,{a}) = RAdj (F,{b})