theorem Lm12a: :: FIELD_15:26

for F being Field
for a being Element of F
for n being Nat holds deg ((X- a) `^ n) = n