:: deftheorem defIm defines Image_hom_Ext_eval FIELD_13:def 3 :
for n being Nat
for F being Field
for E being FieldExtension of F
for x being Function of n,E
for b₅ being strict doubleLoopStr holds
( b₅ = Image_hom_Ext_eval (x,F) iff ( the carrier of b₅ = rng (hom_Ext_eval (x,F)) & the addF of b₅ = the addF of E || (rng (hom_Ext_eval (x,F))) & the multF of b₅ = the multF of E || (rng (hom_Ext_eval (x,F))) & the OneF of b₅ = 1. E & the ZeroF of b₅ = 0. E ) );