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:
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 ;
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 ;
then x in dom (Re f) by ;
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:
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 ;
then x in dom (Im f) by ;
then A24: (Im f) . x = Im (f . x) by COMSEQ_3:def 4;
x in dom (Re f) by ;
then A25: (Re f) . x = Re (f . x) by COMSEQ_3:def 3;
(Im f) . x = (Im a) . n by ;
then A26: Im (f . x) = Im (a . n) by ;
(Re f) . x = (Re a) . n by ;
then Re (f . x) = Re (a . n) by ;
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 ;
hence F,a are_Re-presentation_of f by ; :: thesis: verum