let n be Nat; :: thesis: for F being Field
for E being FieldExtension of F holds E is Polynom-Ring (n,F) -homomorphic
let F be Field; :: thesis: for E being FieldExtension of F holds E is Polynom-Ring (n,F) -homomorphic
let E be FieldExtension of F; :: thesis: E is Polynom-Ring (n,F) -homomorphic
set x = the Function of n,E;
hom_Ext_eval ( the Function of n,E,F) is RingHomomorphism ;
hence E is Polynom-Ring (n,F) -homomorphic ; :: thesis: verum