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 A1: 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 )
len (Im a) = len a by COMPLSP2:48;
then dom (Im a) = Seg (len a) by FINSEQ_1:def 3;
then dom (Im a) = dom a by FINSEQ_1:def 3;
then A2: dom F = dom (Im a) by A1;
dom (Im f) = dom f by COMSEQ_3:def 4;
then A3: dom (Im f) = union (rng F) by A1;
A4: 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 A5: 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 A6: x in F . n ; :: thesis: (Im f) . x = (Im a) . n
F . n c= union (rng F) by A5, MESFUNC3:7;
then x in dom (Im f) by A3, A6;
then A7: (Im f) . x = Im (f . x) by COMSEQ_3:def 4;
Im (f . x) = Im (a . n) by A1, A5, A6;
hence (Im f) . x = (Im a) . n by A2, A5, A7, Th47; :: thesis: verum

end;

len (Re a) = len a by COMPLSP2:48;
then dom (Re a) = Seg (len a) by FINSEQ_1:def 3;
then dom (Re a) = dom a by FINSEQ_1:def 3;
then A8: dom F = dom (Re a) by A1;
dom (Re f) = dom f by COMSEQ_3:def 3;
then A9: dom (Re f) = union (rng F) by A1;
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 A10: 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 A11: x in F . n ; :: thesis: (Re f) . x = (Re a) . n
F . n c= union (rng F) by A10, MESFUNC3:7;
then x in dom (Re f) by A9, A11;
then A12: (Re f) . x = Re (f . x) by COMSEQ_3:def 3;
Re (f . x) = Re (a . n) by A1, A10, A11;
hence (Re f) . x = (Re a) . n by A8, A10, A12, Th46; :: thesis: verum

end;

hence ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) by A9, A3, A8, A2, A4; :: thesis: verum

end;

assume that
A13: F, Re a are_Re-presentation_of Re f and
A14: F, Im a are_Re-presentation_of Im f ; :: thesis: F,a are_Re-presentation_of f
A15: dom F = dom (Re a) by A13;
A16: dom (Re f) = union (rng F) by A13;
then A17: dom f = union (rng F) by COMSEQ_3:def 3;
A18: dom F = dom (Im a) by A14;
A19: dom (Im f) = union (rng F) by A14;
A20: 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 A21: 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 A22: x in F . n ; :: thesis: f . x = a . n
A23: F . n c= union (rng F) by A21, MESFUNC3:7;
then x in dom (Im f) by A19, A22;
then A24: (Im f) . x = Im (f . x) by COMSEQ_3:def 4;
x in dom (Re f) by A16, A22, A23;
then A25: (Re f) . x = Re (f . x) by COMSEQ_3:def 3;
(Im f) . x = (Im a) . n by A14, A21, A22;
then A26: Im (f . x) = Im (a . n) by A18, A21, A24, Th47;
(Re f) . x = (Re a) . n by A13, A21, A22;
then Re (f . x) = Re (a . n) by A15, A21, A25, Th46;
hence f . x = a . n by A26; :: thesis: verum

end;

len (Re a) = len a by COMPLSP2:48;
then dom (Re a) = Seg (len a) by FINSEQ_1:def 3;
then dom F = dom a by A15, FINSEQ_1:def 3;
hence F,a are_Re-presentation_of f by A17, A20; :: thesis: verum