theorem Lm12b: :: FIELD_15:27

for F being Field
for a being Element of F
for n being non zero Nat holds Roots ((X- a) `^ n) = {a}