:: deftheorem Def12 defines Im MESFUN7C:def 12 :
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for b₃ being Functional_Sequence of X,REAL holds
( b₃ = Im f iff for n being Nat holds
( dom (b₃ . n) = dom (f . n) & ( for x being Element of X st x in dom (b₃ . n) holds
(b₃ . n) . x = (Im (f # x)) . n ) ) );