:: deftheorem Def11 defines Re MESFUN7C:def 11 :
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for b₃ being Functional_Sequence of X,REAL holds
( b₃ = Re 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 = (Re (f # x)) . n ) ) );