theorem lemMA: :: FIELD_16:19

for F being Field
for E being FieldExtension of F
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( card (Roots (E,p)) = deg p iff ( p splits_in E & p is separable ) )