theorem mpa1: :: FIELD_14:71

for F being 0 -characteristic Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1