theorem lemphi1: :: FIELD_13:34

for n being Nat
for F, E being Field
for x being Function of n,E holds rng (hom_Ext_eval (x,F)) = { (Ext_eval (p,x)) where p is Polynomial of n,F : verum }