let X be non empty set ; :: thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for x being Element of X st x in dom (f . 0 ) holds
( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )
let f be with_the_same_dom Functional_Sequence of X,COMPLEX ; :: thesis: for x being Element of X st x in dom (f . 0 ) holds
( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )
let x be Element of X; :: thesis: ( x in dom (f . 0 ) implies ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) )
set F = Re f;
set G = Im f;
assume A1: x in dom (f . 0 ) ; :: thesis: ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )

now

let n be Element of NAT ; :: thesis: ( ((Re f) # x) . n = (Re (f # x)) . n & ((Im f) # x) . n = (Im (f # x)) . n )
dom ((Re f) . n) = dom (f . n) by Def11;
then A2: dom ((Re f) . n) = dom (f . 0 ) by MESFUNC8:def 2;
dom ((Im f) . n) = dom (f . n) by Def12;
then A3: dom ((Im f) . n) = dom (f . 0 ) by MESFUNC8:def 2;
( ((Re f) # x) . n = ((Re f) . n) . x & ((Im f) # x) . n = ((Im f) . n) . x ) by SEQFUNC:def 11;
hence ( ((Re f) # x) . n = (Re (f # x)) . n & ((Im f) # x) . n = (Im (f # x)) . n ) by A1, A2, A3, Def11, Def12; :: thesis: verum

end;

hence ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) by FUNCT_2:113; :: thesis: verum