theorem simpmainhelp: :: FIELD_14:75

for F being Field
for K being b₁ -finite FieldExtension of F
for E being b₁ -extending b₁ -finite FieldExtension of F
for a being b₂ -algebraic Element of E st E == FAdj (F,{a}) holds
( E == FAdj (K,{a}) & K == FAdj (F,(Coeff (MinPoly (a,K)))) )