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 ) )

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

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

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 that 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

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

end;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

len (Re a) = len a
by COMPLSP2:48;
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;(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

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

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
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;(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

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

len (Re a) = len a
by COMPLSP2:48;
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;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

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