theorem helpp: :: FIELD_13:33

for n being Nat
for F being Field
for E being FieldExtension of F holds E is Polynom-Ring (n,F) -homomorphic