theorem lems1: :: FIELD_15:61

for F being Field
for E being FieldExtension of F
for p being non zero Polynomial of F
for c being non zero Element of F
for a being Element of E holds multiplicity ((c * p),a) = multiplicity (p,a)