let X be non empty set ; :: thesis: for f being Functional_Sequence of X,COMPLEX
for n being Nat 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 Nat holds
( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
let n be Nat; :: thesis: ( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
dom ((Re f) . n) = dom (f . n) by Def11;
then A1: dom ((Re f) . n) = dom (Re (f . n)) by COMSEQ_3:def 3;
now :: thesis: for x being Element of X st x in dom ((Re f) . n) holds
((Re f) . n) . x = (Re (f . n)) . x
let x be Element of X; :: thesis: ( x in dom ((Re f) . n) implies ((Re f) . n) . x = (Re (f . n)) . x )
assume A2: 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 A1, COMSEQ_3:def 3;
then A3: (Re (f . n)) . x = Re ((f # x) . n) by Def9;
((Re f) . n) . x = (Re (f # x)) . n by A2, Def11;
hence ((Re f) . n) . x = (Re (f . n)) . x by A3, COMSEQ_3:def 5; :: thesis: verum
end;
hence (Re f) . n = Re (f . n) by A1, PARTFUN1:5; :: thesis: (Im f) . n = Im (f . n)
dom ((Im f) . n) = dom (f . n) by Def12;
then A4: dom ((Im f) . n) = dom (Im (f . n)) by COMSEQ_3:def 4;
now :: thesis: for x being Element of X st x in dom ((Im f) . n) holds
((Im f) . n) . x = (Im (f . n)) . x
let x be Element of X; :: thesis: ( x in dom ((Im f) . n) implies ((Im f) . n) . x = (Im (f . n)) . x )
assume A5: 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 A4, COMSEQ_3:def 4;
then A6: (Im (f . n)) . x = Im ((f # x) . n) by Def9;
((Im f) . n) . x = (Im (f # x)) . n by A5, Def12;
hence ((Im f) . n) . x = (Im (f . n)) . x by A6, COMSEQ_3:def 6; :: thesis: verum
end;
hence (Im f) . n = Im (f . n) by A4, PARTFUN1:5; :: thesis: verum