let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for F being Finite_Sep_Sequence of S
for a being FinSequence of COMPLEX holds
( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )
let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX
for F being Finite_Sep_Sequence of S
for a being FinSequence of COMPLEX holds
( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )
let f be PartFunc of X,COMPLEX ; :: thesis: for F being Finite_Sep_Sequence of S
for a being FinSequence of COMPLEX holds
( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )
let F be Finite_Sep_Sequence of S; :: thesis: for a being FinSequence of COMPLEX holds
( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )
let a be FinSequence of COMPLEX ; :: thesis: ( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )

hereby :: thesis: ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f implies F,a are_Re-presentation_of f )

assume AS1: F,a are_Re-presentation_of f ; :: thesis: ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f )
( dom (Re f) = dom f & dom (Im f) = dom f ) by MESFUN6C:def 1, MESFUN6C:def 2;
then B1: ( dom (Re f) = union (rng F) & dom (Im f) = union (rng F) ) by AS1, MES3Cdef1;
( len (Re a) = len a & len (Im a) = len a ) by COMPLSP2:48;
then ( dom (Re a) = Seg (len a) & dom (Im a) = Seg (len a) ) by FINSEQ_1:def 3;
then ( dom (Re a) = dom a & dom (Im a) = dom a ) by FINSEQ_1:def 3;
then B2: ( dom F = dom (Re a) & dom F = dom (Im a) ) by AS1, MES3Cdef1;
B3: for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re a) . n

proof

let n be Nat; :: thesis: ( n in dom F implies for x being set st x in F . n holds
(Re f) . x = (Re a) . n )
assume P01: n in dom F ; :: thesis: for x being set st x in F . n holds
(Re f) . x = (Re a) . n
let x be set ; :: thesis: ( x in F . n implies (Re f) . x = (Re a) . n )
assume P02: x in F . n ; :: thesis: (Re f) . x = (Re a) . n
F . n c= union (rng F) by P01, MESFUNC3:7;
then x in dom (Re f) by P02, B1;
then P05: (Re f) . x = Re (f . x) by MESFUN6C:def 1;
Re (f . x) = Re (a . n) by P01, P02, AS1, MES3Cdef1;
hence (Re f) . x = (Re a) . n by P01, B2, Def31, P05; :: thesis: verum

end;

for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im a) . n

proof

let n be Nat; :: thesis: ( n in dom F implies for x being set st x in F . n holds
(Im f) . x = (Im a) . n )
assume P01: n in dom F ; :: thesis: for x being set st x in F . n holds
(Im f) . x = (Im a) . n
let x be set ; :: thesis: ( x in F . n implies (Im f) . x = (Im a) . n )
assume P02: x in F . n ; :: thesis: (Im f) . x = (Im a) . n
F . n c= union (rng F) by P01, MESFUNC3:7;
then x in dom (Im f) by P02, B1;
then P05: (Im f) . x = Im (f . x) by MESFUN6C:def 2;
Im (f . x) = Im (a . n) by P02, P01, AS1, MES3Cdef1;
hence (Im f) . x = (Im a) . n by P01, B2, Def32, P05; :: thesis: verum

end;

hence ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) by B1, B2, B3, MES3def1; :: thesis: verum

end;

assume AS1: ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) ; :: thesis: F,a are_Re-presentation_of f
A1: ( dom (Re f) = union (rng F) & dom (Im f) = union (rng F) ) by AS1, MES3def1;
A2: ( dom F = dom (Re a) & dom F = dom (Im a) ) by AS1, MES3def1;
B1: dom f = union (rng F) by A1, MESFUN6C:def 1;
len (Re a) = len a by COMPLSP2:48;
then dom (Re a) = Seg (len a) by FINSEQ_1:def 3;
then B2: dom F = dom a by A2, FINSEQ_1:def 3;
for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n

proof

let n be Nat; :: thesis: ( n in dom F implies for x being set st x in F . n holds
f . x = a . n )
assume P01: n in dom F ; :: thesis: for x being set st x in F . n holds
f . x = a . n
let x be set ; :: thesis: ( x in F . n implies f . x = a . n )
assume P02: x in F . n ; :: thesis: f . x = a . n
P03: F . n c= union (rng F) by P01, MESFUNC3:7;
then x in dom (Re f) by P02, A1;
then P04: (Re f) . x = Re (f . x) by MESFUN6C:def 1;
(Re f) . x = (Re a) . n by P01, P02, AS1, MES3def1;
then P05: Re (f . x) = Re (a . n) by P01, A2, Def31, P04;
x in dom (Im f) by P02, P03, A1;
then P06: (Im f) . x = Im (f . x) by MESFUN6C:def 2;
(Im f) . x = (Im a) . n by P01, P02, AS1, MES3def1;
then Im (f . x) = Im (a . n) by P01, A2, Def32, P06;
hence f . x = a . n by P05, COMPLEX1:def 5; :: thesis: verum

end;

hence F,a are_Re-presentation_of f by B1, B2, MES3Cdef1; :: thesis: verum