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) )
A1: n in NAT by ORDINAL1:def 13;
dom ((Re f) . n) = dom (f . n) by Def11;
then A2: dom ((Re f) . n) = dom (Re (f . n)) by MESFUN6C:def 1;

now

let x be Element of X; :: thesis: ( x in dom ((Re f) . n) implies ((Re f) . n) . x = (Re (f . n)) . x )
assume A3: x in dom ((Re f) . n) ; :: thesis: ((Re f) . n) . x = (Re (f . n)) . x
then (Re (f . n)) . x = Re ((f . n) . x) by A2, MESFUN6C:def 1;
then A4: (Re (f . n)) . x = Re ((f # x) . n) by Def9;
((Re f) . n) . x = (Re (f # x)) . n by A3, Def11;
hence ((Re f) . n) . x = (Re (f . n)) . x by A1, A4, COMSEQ_3:def 3; :: thesis: verum

end;

hence (Re f) . n = Re (f . n) by A2, PARTFUN1:34; :: thesis: (Im f) . n = Im (f . n)
dom ((Im f) . n) = dom (f . n) by Def12;
then A5: dom ((Im f) . n) = dom (Im (f . n)) by MESFUN6C:def 2;

now

let x be Element of X; :: thesis: ( x in dom ((Im f) . n) implies ((Im f) . n) . x = (Im (f . n)) . x )
assume A6: x in dom ((Im f) . n) ; :: thesis: ((Im f) . n) . x = (Im (f . n)) . x
then (Im (f . n)) . x = Im ((f . n) . x) by A5, MESFUN6C:def 2;
then A7: (Im (f . n)) . x = Im ((f # x) . n) by Def9;
((Im f) . n) . x = (Im (f # x)) . n by A6, Def12;
hence ((Im f) . n) . x = (Im (f . n)) . x by A1, A7, COMSEQ_3:def 4; :: thesis: verum

end;

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