theorem ro0: :: FIELD_15:28

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