let X be non empty set ; :: thesis: for f being Functional_Sequence of X,COMPLEX
for n being natural number holds
( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
let f be Functional_Sequence of X,COMPLEX ; :: thesis: for n being natural number holds
( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
let n be natural number ; :: thesis: ( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
( dom ((Re f) . n) = dom (f . n) & dom ((Im f) . n) = dom (f . n) ) by Def13, Def14;
then B2: ( dom ((Re f) . n) = dom (Re (f . n)) & dom ((Im f) . n) = dom (Im (f . n)) ) by MESFUN6C:def 1, MESFUN6C:def 2;
B3: n in NAT by ORDINAL1:def 13;

now

let x be Element of X; :: thesis: ( x in dom ((Re f) . n) implies ((Re f) . n) . x = (Re (f . n)) . x )
assume P01: x in dom ((Re f) . n) ; :: thesis: ((Re f) . n) . x = (Re (f . n)) . x
then P02: ((Re f) . n) . x = (Re (f # x)) . n by Def13;
(Re (f . n)) . x = Re ((f . n) . x) by P01, B2, MESFUN6C:def 1;
then (Re (f . n)) . x = Re ((f # x) . n) by Def11;
hence ((Re f) . n) . x = (Re (f . n)) . x by B3, P02, COMSEQ_3:def 3; :: thesis: verum

end;

hence (Re f) . n = Re (f . n) by B2, PARTFUN1:34; :: thesis: (Im f) . n = Im (f . n)

now

let x be Element of X; :: thesis: ( x in dom ((Im f) . n) implies ((Im f) . n) . x = (Im (f . n)) . x )
assume P01: x in dom ((Im f) . n) ; :: thesis: ((Im f) . n) . x = (Im (f . n)) . x
then P02: ((Im f) . n) . x = (Im (f # x)) . n by Def14;
(Im (f . n)) . x = Im ((f . n) . x) by P01, B2, MESFUN6C:def 2;
then (Im (f . n)) . x = Im ((f # x) . n) by Def11;
hence ((Im f) . n) . x = (Im (f . n)) . x by B3, P02, COMSEQ_3:def 4; :: thesis: verum

end;

hence (Im f) . n = Im (f . n) by B2, PARTFUN1:34; :: thesis: verum