set E = the FieldExtension of F;
set a = the Element of the FieldExtension of F;
take the FieldExtension of F ; :: thesis: the FieldExtension of F is Polynom-Ring F -homomorphic
thus the FieldExtension of F is Polynom-Ring F -homomorphic ; :: thesis: verum