theorem lemphi3: :: FIELD_13:35

for n being Nat
for F being Field
for E being FieldExtension of F
for x being Function of n,E holds F is Subring of Image_hom_Ext_eval (x,F)