:: The Measurability of Complex-Valued Functional Sequences
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Copyright (c) 2008-2021 Association of Mizar Users

definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func R_EAL f -> Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 1
f;
coherence
f is Functional_Sequence of X,ExtREAL
proof end;
end;

:: deftheorem defines R_EAL MESFUN7C:def 1 :
for X being non empty set
for f being Functional_Sequence of X,REAL holds R_EAL f = f;

theorem Th1: :: MESFUN7C:1
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X holds f # x = () # x
proof end;

registration
let X be non empty set ;
let f be Function of X,REAL;
coherence
R_EAL f is total
;
end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func inf f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 2
inf ();
coherence
inf () is PartFunc of X,ExtREAL
;
end;

:: deftheorem defines inf MESFUN7C:def 2 :
for X being non empty set
for f being Functional_Sequence of X,REAL holds inf f = inf ();

theorem Th2: :: MESFUN7C:2
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (inf f) holds
(inf f) . x = inf (rng (R_EAL (f # x)))
proof end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func sup f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 3
sup ();
coherence
sup () is PartFunc of X,ExtREAL
;
end;

:: deftheorem defines sup MESFUN7C:def 3 :
for X being non empty set
for f being Functional_Sequence of X,REAL holds sup f = sup ();

theorem Th3: :: MESFUN7C:3
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (sup f) holds
(sup f) . x = sup (rng (R_EAL (f # x)))
proof end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
coherence ;
end;

:: deftheorem defines inferior_realsequence MESFUN7C:def 4 :
for X being non empty set
for f being Functional_Sequence of X,REAL holds inferior_realsequence f = inferior_realsequence ();

theorem Th4: :: MESFUN7C:4
for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom () = dom (f . 0) & ( for x being Element of X st x in dom () holds
() . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
proof end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
coherence ;
end;

:: deftheorem defines superior_realsequence MESFUN7C:def 5 :
for X being non empty set
for f being Functional_Sequence of X,REAL holds superior_realsequence f = superior_realsequence ();

theorem Th5: :: MESFUN7C:5
for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom () = dom (f . 0) & ( for x being Element of X st x in dom () holds
() . x = (superior_realsequence (R_EAL (f # x))) . n ) )
proof end;

theorem :: MESFUN7C:6
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) holds
# x = inferior_realsequence (R_EAL (f # x))
proof end;

registration
let X be non empty set ;
let f be with_the_same_dom Functional_Sequence of X,REAL;
coherence
proof end;
end;

theorem Th7: :: MESFUN7C:7
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,REAL
for S being SigmaField of X
for E being Element of S
for n being Nat st f . n is E -measurable holds
() . n is E -measurable
proof end;

theorem :: MESFUN7C:8
for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds () ^\ n = R_EAL (f ^\ n) ;

theorem :: MESFUN7C:9
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,REAL
for n being Nat holds . n = inf (f ^\ n) by MESFUNC8:8;

theorem :: MESFUN7C:10
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,REAL
for n being Nat holds . n = sup (f ^\ n) by MESFUNC8:9;

theorem Th11: :: MESFUN7C:11
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) holds
# x = superior_realsequence (R_EAL (f # x))
proof end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func lim_inf f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 6
lim_inf ();
coherence
lim_inf () is PartFunc of X,ExtREAL
;
end;

:: deftheorem defines lim_inf MESFUN7C:def 6 :
for X being non empty set
for f being Functional_Sequence of X,REAL holds lim_inf f = lim_inf ();

theorem Th12: :: MESFUN7C:12
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom () holds
() . x = lim_inf (R_EAL (f # x))
proof end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func lim_sup f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 7
lim_sup ();
coherence
lim_sup () is PartFunc of X,ExtREAL
;
end;

:: deftheorem defines lim_sup MESFUN7C:def 7 :
for X being non empty set
for f being Functional_Sequence of X,REAL holds lim_sup f = lim_sup ();

theorem Th13: :: MESFUN7C:13
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom () holds
() . x = lim_sup (R_EAL (f # x))
proof end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func lim f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 8
lim ();
coherence
lim () is PartFunc of X,ExtREAL
;
end;

:: deftheorem defines lim MESFUN7C:def 8 :
for X being non empty set
for f being Functional_Sequence of X,REAL holds lim f = lim ();

theorem Th14: :: MESFUN7C:14
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim f) holds
(lim f) . x = lim (R_EAL (f # x))
proof end;

theorem Th15: :: MESFUN7C:15
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim f) & f # x is convergent holds
( (lim f) . x = () . x & (lim f) . x = () . x )
proof end;

theorem :: MESFUN7C:16
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))
proof end;

theorem :: MESFUN7C:17
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
proof end;

theorem Th18: :: MESFUN7C:18
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds
lim_sup f is E -measurable
proof end;

theorem :: MESFUN7C:19
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds
lim_inf f is E -measurable
proof end;

theorem :: MESFUN7C:20
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) & f # x is convergent holds
# x is bounded_below
proof end;

theorem Th21: :: MESFUN7C:21
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is E -measurable
proof end;

theorem Th22: :: MESFUN7C:22
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is E -measurable
proof end;

definition
let X be non empty set ;
let H be Functional_Sequence of X,COMPLEX;
let x be Element of X;
func H # x -> Complex_Sequence means :Def9: :: MESFUN7C:def 9
for n being Nat holds it . n = (H . n) . x;
existence
ex b1 being Complex_Sequence st
for n being Nat holds b1 . n = (H . n) . x
proof end;
uniqueness
for b1, b2 being Complex_Sequence st ( for n being Nat holds b1 . n = (H . n) . x ) & ( for n being Nat holds b2 . n = (H . n) . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines # MESFUN7C:def 9 :
for X being non empty set
for H being Functional_Sequence of X,COMPLEX
for x being Element of X
for b4 being Complex_Sequence holds
( b4 = H # x iff for n being Nat holds b4 . n = (H . n) . x );

definition
let X be non empty set ;
let f be Functional_Sequence of X,COMPLEX;
func lim f -> PartFunc of X,COMPLEX means :Def10: :: MESFUN7C:def 10
( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds
it . x = lim (f # x) ) );
existence
ex b1 being PartFunc of X,COMPLEX st
( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = lim (f # x) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of X,COMPLEX st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = lim (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds
b2 . x = lim (f # x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines lim MESFUN7C:def 10 :
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for b3 being PartFunc of X,COMPLEX holds
( b3 = lim f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds
b3 . x = lim (f # x) ) ) );

definition
let X be non empty set ;
let f be Functional_Sequence of X,COMPLEX;
func Re f -> Functional_Sequence of X,REAL means :Def11: :: MESFUN7C:def 11
for n being Nat holds
( dom (it . n) = dom (f . n) & ( for x being Element of X st x in dom (it . n) holds
(it . n) . x = (Re (f # x)) . n ) );
existence
ex b1 being Functional_Sequence of X,REAL st
for n being Nat holds
( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (Re (f # x)) . n ) )
proof end;
uniqueness
for b1, b2 being Functional_Sequence of X,REAL st ( for n being Nat holds
( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (Re (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (b2 . n) = dom (f . n) & ( for x being Element of X st x in dom (b2 . n) holds
(b2 . n) . x = (Re (f # x)) . n ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines Re MESFUN7C:def 11 :
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for b3 being Functional_Sequence of X,REAL holds
( b3 = Re f iff for n being Nat holds
( dom (b3 . n) = dom (f . n) & ( for x being Element of X st x in dom (b3 . n) holds
(b3 . n) . x = (Re (f # x)) . n ) ) );

registration
let X be non empty set ;
let f be with_the_same_dom Functional_Sequence of X,COMPLEX;
correctness
coherence ;
proof end;
end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,COMPLEX;
func Im f -> Functional_Sequence of X,REAL means :Def12: :: MESFUN7C:def 12
for n being Nat holds
( dom (it . n) = dom (f . n) & ( for x being Element of X st x in dom (it . n) holds
(it . n) . x = (Im (f # x)) . n ) );
existence
ex b1 being Functional_Sequence of X,REAL st
for n being Nat holds
( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (Im (f # x)) . n ) )
proof end;
uniqueness
for b1, b2 being Functional_Sequence of X,REAL st ( for n being Nat holds
( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (Im (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (b2 . n) = dom (f . n) & ( for x being Element of X st x in dom (b2 . n) holds
(b2 . n) . x = (Im (f # x)) . n ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines Im MESFUN7C:def 12 :
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for b3 being Functional_Sequence of X,REAL holds
( b3 = Im f iff for n being Nat holds
( dom (b3 . n) = dom (f . n) & ( for x being Element of X st x in dom (b3 . n) holds
(b3 . n) . x = (Im (f # x)) . n ) ) );

registration
let X be non empty set ;
let f be with_the_same_dom Functional_Sequence of X,COMPLEX;
correctness
coherence ;
proof end;
end;

theorem Th23: :: MESFUN7C:23
for X being non empty set
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) )
proof end;

theorem Th24: :: MESFUN7C:24
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
proof end;

theorem Th25: :: MESFUN7C:25
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,COMPLEX st ( for x being Element of X st x in dom (f . 0) holds
f # x is convergent ) holds
( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )
proof end;

theorem :: MESFUN7C:26
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is E -measurable
proof end;

theorem :: MESFUN7C:27
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for g being PartFunc of X,COMPLEX
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is E -measurable
proof end;

theorem :: MESFUN7C:28
for X being non empty set
for Y being set
for f being PartFunc of X,COMPLEX
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
proof end;

Lm1: for X being non empty set
for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative

proof end;

theorem :: MESFUN7C:29
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for k being Real
for E being Element of S st 0 <= k & E c= dom f & f is E -measurable holds
|.f.| to_power k is E -measurable
proof end;

theorem Th30: :: MESFUN7C:30
for X being non empty set
for f, g being PartFunc of X,REAL holds () (#) () = R_EAL (f (#) g)
proof end;

theorem Th31: :: MESFUN7C:31
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is E -measurable & g is E -measurable holds
f (#) g is E -measurable
proof end;

theorem Th32: :: MESFUN7C:32
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds
( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )
proof end;

theorem :: MESFUN7C:33
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for E being Element of S st (dom f) /\ (dom g) = E & f is E -measurable & g is E -measurable holds
f (#) g is E -measurable
proof end;

theorem Th34: :: MESFUN7C:34
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex E being Element of S st
( E = dom f & E = dom g & f is E -measurable & g is E -measurable ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) holds
Integral (M,g) <= Integral (M,f)
proof end;

theorem Th35: :: MESFUN7C:35
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
( ex A being Element of S st
( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M )
proof end;

theorem :: MESFUN7C:36
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being sequence of S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
proof end;

theorem Th37: :: MESFUN7C:37
for X being non empty set
for f being PartFunc of X,COMPLEX
for A being set holds |.f.| | A = |.(f | A).|
proof end;

theorem Th38: :: MESFUN7C:38
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds
( dom () = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
proof end;

theorem Th39: :: MESFUN7C:39
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = () | (dom |.(f + g).|)
proof end;

theorem Th40: :: MESFUN7C:40
for X being non empty set
for f, g being PartFunc of X,COMPLEX
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= () . x
proof end;

theorem Th41: :: MESFUN7C:41
for X being non empty set
for f, g being PartFunc of X,REAL st ( for x being set st x in dom f holds
f . x <= g . x ) holds
g - f is nonnegative
proof end;

theorem :: MESFUN7C:42
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,COMPLEX;
pred f is_simple_func_in S means :: MESFUN7C:def 13
ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) );
end;

:: deftheorem defines is_simple_func_in MESFUN7C:def 13 :
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) ) );

definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,REAL;
let F be Finite_Sep_Sequence of S;
let a be FinSequence of REAL ;
pred F,a are_Re-presentation_of f means :: MESFUN7C:def 14
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) );
end;

:: deftheorem defines are_Re-presentation_of MESFUN7C:def 14 :
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of REAL holds
( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) );

definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,COMPLEX;
let F be Finite_Sep_Sequence of S;
let a be FinSequence of COMPLEX ;
pred F,a are_Re-presentation_of f means :: MESFUN7C:def 15
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) );
end;

:: deftheorem defines are_Re-presentation_of MESFUN7C:def 15 :
for X being non empty set
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 ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) );

theorem :: MESFUN7C:43
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )
proof end;

theorem Th44: :: MESFUN7C:44
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( 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 end;

theorem Th45: :: MESFUN7C:45
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )
proof end;

theorem Th46: :: MESFUN7C:46
for c being FinSequence of COMPLEX
for n being Nat st n in dom (Re c) holds
(Re c) . n = Re (c . n)
proof end;

theorem Th47: :: MESFUN7C:47
for c being FinSequence of COMPLEX
for n being Nat st n in dom (Im c) holds
(Im c) . n = Im (c . n)
proof end;

theorem Th48: :: MESFUN7C:48
for X being non empty set
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 ) )
proof end;

theorem :: MESFUN7C:49
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) ) )
proof end;