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 :: thesis: for n being Element of NAT holds
( ((Re f) # x) . n = (Re (f # x)) . n & ((Im f) # x) . n = (Im (f # x)) . n )

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 10;
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:63; :: thesis: verum