:: MESFUN7C semantic presentation

begin


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
 ( dom f = NAT & ( for n being Element of NAT holds f . n is PartFunc of X,ExtREAL ) ) by NUMBERS:31, RELSET_1:7, SEQFUNC:1;
hence  f is Functional_Sequence of X,ExtREAL by SEQFUNC:1; ::_thesis: verum
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 = (R_EAL f) # x
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X holds f # x = (R_EAL f) # x
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X holds f # x = (R_EAL f) # x
let x be Element of X; ::_thesis: f # x = (R_EAL f) # x
now__::_thesis:_for_r_being_set_st_r_in_rng_((R_EAL_f)_#_x)_holds_
r_in_REAL
let r be set ; ::_thesis: ( r in rng ((R_EAL f) # x) implies r in REAL )
assume  r in rng ((R_EAL f) # x) ; ::_thesis: r in REAL
then consider n being set  such that
A1: n in NAT and
A2: ((R_EAL f) # x) . n = r by FUNCT_2:11;
reconsider n = n as Element of NAT by A1;
r = ((R_EAL f) . n) . x by A2, MESFUNC5:def_13
.= (R_EAL (f . n)) . x
.= (f . n) . x ;
hence  r in REAL ; ::_thesis: verum
end;
then  rng ((R_EAL f) # x) c= REAL by TARSKI:def_3;
then reconsider RFx = (R_EAL f) # x as Function of NAT,REAL by FUNCT_2:6;
reconsider RFx = RFx as Real_Sequence ;
now__::_thesis:_for_n_being_set_st_n_in_NAT_holds_
RFx_._n_=_(f_#_x)_._n
let n be set ; ::_thesis: ( n in NAT implies RFx . n = (f # x) . n )
assume  n in NAT ; ::_thesis: RFx . n = (f # x) . n
then reconsider n1 = n as Element of NAT ;
RFx . n = ((R_EAL f) . n1) . x by MESFUNC5:def_13
.= (R_EAL (f . n1)) . x ;
hence  RFx . n = (f # x) . n by SEQFUNC:def_10; ::_thesis: verum
end;
hence  f # x = (R_EAL f) # x by FUNCT_2:12; ::_thesis: verum
end;

registration
let X be non empty set ;
let f be Function of X,REAL;
cluster R_EAL f ->  total ;
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 (R_EAL f);
coherence
 inf (R_EAL f) 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 (R_EAL f);

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
let X be non empty set ; ::_thesis: 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)))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (inf f) holds
(inf f) . x = inf (rng (R_EAL (f # x)))
let x be Element of X; ::_thesis: ( x in dom (inf f) implies (inf f) . x = inf (rng (R_EAL (f # x))) )
assume  x in dom (inf f) ; ::_thesis: (inf f) . x = inf (rng (R_EAL (f # x)))
then  (inf f) . x = inf ((R_EAL f) # x) by MESFUNC8:def_3;
hence  (inf f) . x = inf (rng (R_EAL (f # x))) by Th1; ::_thesis: verum
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 (R_EAL f);
coherence
 sup (R_EAL f) 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 (R_EAL f);

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
let X be non empty set ; ::_thesis: 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)))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (sup f) holds
(sup f) . x = sup (rng (R_EAL (f # x)))
let x be Element of X; ::_thesis: ( x in dom (sup f) implies (sup f) . x = sup (rng (R_EAL (f # x))) )
assume  x in dom (sup f) ; ::_thesis: (sup f) . x = sup (rng (R_EAL (f # x)))
then  (sup f) . x = sup ((R_EAL f) # x) by MESFUNC8:def_4;
hence  (sup f) . x = sup (rng (R_EAL (f # x))) by Th1; ::_thesis: verum
end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func inferior_realsequence f ->  with_the_same_dom Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 4
 inferior_realsequence (R_EAL f);
coherence
 inferior_realsequence (R_EAL f) is with_the_same_dom Functional_Sequence of X,ExtREAL ;
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 (R_EAL f);

theorem Th4: :: MESFUN7C:4
for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
let f be Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds
( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
let n be Nat; ::_thesis: ( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
set IF = inferior_realsequence f;
dom ((inferior_realsequence f) . n) = dom ((R_EAL f) . 0) by MESFUNC8:def_5
.= dom (R_EAL (f . 0)) ;
hence  dom ((inferior_realsequence f) . n) = dom (f . 0) ; ::_thesis: for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n
A1: n in NAT by ORDINAL1:def_12;
hereby  ::_thesis: verum
let x be Element of X; ::_thesis: ( x in dom ((inferior_realsequence f) . n) implies ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n )
assume  x in dom ((inferior_realsequence f) . n) ; ::_thesis: ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n
then A2: ((inferior_realsequence f) . n) . x = (inferior_realsequence ((R_EAL f) # x)) . n by MESFUNC8:def_5
.= inf (((R_EAL f) # x) ^\ n) by A1, RINFSUP2:27 ;
 (R_EAL f) # x = f # x by Th1;
hence  ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n by A1, A2, RINFSUP2:27; ::_thesis: verum
end;
end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func superior_realsequence f ->  with_the_same_dom Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 5
 superior_realsequence (R_EAL f);
coherence
 superior_realsequence (R_EAL f) is with_the_same_dom Functional_Sequence of X,ExtREAL ;
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 (R_EAL f);

theorem Th5: :: MESFUN7C:5
for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )
let f be Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds
( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )
let n be Nat; ::_thesis: ( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )
set SF = superior_realsequence f;
thus  dom ((superior_realsequence f) . n) = dom (f . 0) by MESFUNC8:def_6; ::_thesis: for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n
hereby  ::_thesis: verum
let x be Element of X; ::_thesis: ( x in dom ((superior_realsequence f) . n) implies ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n )
assume  x in dom ((superior_realsequence f) . n) ; ::_thesis: ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n
then  ((superior_realsequence f) . n) . x = (superior_realsequence ((R_EAL f) # x)) . n by MESFUNC8:def_6;
hence  ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n by Th1; ::_thesis: verum
end;
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
(inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) holds
(inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds
(inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))
let x be Element of X; ::_thesis: ( x in dom (f . 0) implies (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) )
set F = inferior_realsequence f;
assume A1: x in dom (f . 0) ; ::_thesis: (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))
now__::_thesis:_for_n_being_Element_of_NAT_holds_((inferior_realsequence_f)_#_x)_._n_=_(inferior_realsequence_(R_EAL_(f_#_x)))_._n
let n be Element of NAT ; ::_thesis: ((inferior_realsequence f) # x) . n = (inferior_realsequence (R_EAL (f # x))) . n
 ( dom ((inferior_realsequence f) . n) = dom (f . 0) & ((inferior_realsequence f) # x) . n = ((inferior_realsequence f) . n) . x ) by Th4, MESFUNC5:def_13;
hence  ((inferior_realsequence f) # x) . n = (inferior_realsequence (R_EAL (f # x))) . n by A1, Th4; ::_thesis: verum
end;
hence  (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) by FUNCT_2:63; ::_thesis: verum
end;

registration
let X be non empty set ;
let f be with_the_same_dom Functional_Sequence of X,REAL;
cluster R_EAL f ->  with_the_same_dom ;
coherence
 R_EAL f is with_the_same_dom
proof
 for n, m being Nat holds dom ((R_EAL f) . n) = dom ((R_EAL f) . m) by MESFUNC8:def_2;
hence  R_EAL f is with_the_same_dom by MESFUNC8:def_2; ::_thesis: verum
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_measurable_on E holds
(R_EAL f) . n is_measurable_on E
proof
let X be non empty set ; ::_thesis: 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_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for S being SigmaField of X
for E being Element of S
for n being Nat st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for n being Nat st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let E be Element of S; ::_thesis: for n being Nat st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let n be Nat; ::_thesis: ( f . n is_measurable_on E implies (R_EAL f) . n is_measurable_on E )
assume  f . n is_measurable_on E ; ::_thesis: (R_EAL f) . n is_measurable_on E
then  R_EAL (f . n) is_measurable_on E by MESFUNC6:def_1;
hence  (R_EAL f) . n is_measurable_on E ; ::_thesis: verum
end;

theorem :: MESFUN7C:8
for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds (R_EAL f) ^\ 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 (inferior_realsequence f) . n = inf (f ^\ n)
proof
let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n)
let n be Nat; ::_thesis: (inferior_realsequence f) . n = inf (f ^\ n)
 n in NAT by ORDINAL1:def_12;
then  (inferior_realsequence (R_EAL f)) . n = inf ((R_EAL f) ^\ n) by MESFUNC8:8;
hence  (inferior_realsequence f) . n = inf (f ^\ n) ; ::_thesis: verum
end;

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 (superior_realsequence f) . n = sup (f ^\ n)
proof
let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n)
let n be Nat; ::_thesis: (superior_realsequence f) . n = sup (f ^\ n)
 n in NAT by ORDINAL1:def_12;
then  (superior_realsequence (R_EAL f)) . n = sup ((R_EAL f) ^\ n) by MESFUNC8:9;
hence  (superior_realsequence f) . n = sup (f ^\ n) ; ::_thesis: verum
end;

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
(superior_realsequence f) # x = superior_realsequence (R_EAL (f # x))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) holds
(superior_realsequence f) # x = superior_realsequence (R_EAL (f # x))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds
(superior_realsequence f) # x = superior_realsequence (R_EAL (f # x))
let x be Element of X; ::_thesis: ( x in dom (f . 0) implies (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x)) )
set F = superior_realsequence f;
assume A1: x in dom (f . 0) ; ::_thesis: (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x))
now__::_thesis:_for_n_being_Element_of_NAT_holds_((superior_realsequence_f)_#_x)_._n_=_(superior_realsequence_(R_EAL_(f_#_x)))_._n
let n be Element of NAT ; ::_thesis: ((superior_realsequence f) # x) . n = (superior_realsequence (R_EAL (f # x))) . n
 ( dom ((superior_realsequence f) . n) = dom (f . 0) & ((superior_realsequence f) # x) . n = ((superior_realsequence f) . n) . x ) by Th5, MESFUNC5:def_13;
hence  ((superior_realsequence f) # x) . n = (superior_realsequence (R_EAL (f # x))) . n by A1, Th5; ::_thesis: verum
end;
hence  (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x)) by FUNCT_2:63; ::_thesis: verum
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 (R_EAL f);
coherence
 lim_inf (R_EAL f) 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 (R_EAL f);

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 (lim_inf f) holds
(lim_inf f) . x = lim_inf (R_EAL (f # x))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim_inf f) holds
(lim_inf f) . x = lim_inf (R_EAL (f # x))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim_inf f) holds
(lim_inf f) . x = lim_inf (R_EAL (f # x))
let x be Element of X; ::_thesis: ( x in dom (lim_inf f) implies (lim_inf f) . x = lim_inf (R_EAL (f # x)) )
assume  x in dom (lim_inf f) ; ::_thesis: (lim_inf f) . x = lim_inf (R_EAL (f # x))
then  (lim_inf f) . x = lim_inf ((R_EAL f) # x) by MESFUNC8:def_7;
hence  (lim_inf f) . x = lim_inf (R_EAL (f # x)) by Th1; ::_thesis: verum
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 (R_EAL f);
coherence
 lim_sup (R_EAL f) 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 (R_EAL f);

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 (lim_sup f) holds
(lim_sup f) . x = lim_sup (R_EAL (f # x))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim_sup f) holds
(lim_sup f) . x = lim_sup (R_EAL (f # x))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim_sup f) holds
(lim_sup f) . x = lim_sup (R_EAL (f # x))
let x be Element of X; ::_thesis: ( x in dom (lim_sup f) implies (lim_sup f) . x = lim_sup (R_EAL (f # x)) )
assume  x in dom (lim_sup f) ; ::_thesis: (lim_sup f) . x = lim_sup (R_EAL (f # x))
then  (lim_sup f) . x = lim_sup ((R_EAL f) # x) by MESFUNC8:def_8;
hence  (lim_sup f) . x = lim_sup (R_EAL (f # x)) by Th1; ::_thesis: verum
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 (R_EAL f);
coherence
 lim (R_EAL f) 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 (R_EAL f);

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
let X be non empty set ; ::_thesis: 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))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim f) holds
(lim f) . x = lim (R_EAL (f # x))
let x be Element of X; ::_thesis: ( x in dom (lim f) implies (lim f) . x = lim (R_EAL (f # x)) )
assume  x in dom (lim f) ; ::_thesis: (lim f) . x = lim (R_EAL (f # x))
then  (lim f) . x = lim ((R_EAL f) # x) by MESFUNC8:def_9;
hence  (lim f) . x = lim (R_EAL (f # x)) by Th1; ::_thesis: verum
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 = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
proof
let X be non empty set ; ::_thesis: 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 = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim f) & f # x is convergent holds
( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
let x be Element of X; ::_thesis: ( x in dom (lim f) & f # x is convergent implies ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) )
assume that
A1: x in dom (lim f) and
A2: f # x is convergent ; ::_thesis: ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
 R_EAL (f # x) is convergent by A2, RINFSUP2:14;
then A3: ( lim (R_EAL (f # x)) = lim_sup (R_EAL (f # x)) & lim (R_EAL (f # x)) = lim_inf (R_EAL (f # x)) ) by RINFSUP2:41;
A4: x in dom (f . 0) by A1, MESFUNC8:def_9;
then  x in dom (lim_inf f) by MESFUNC8:def_7;
then A5: (lim_inf f) . x = lim_inf (R_EAL (f # x)) by Th12;
 x in dom (lim_sup f) by A4, MESFUNC8:def_8;
then  (lim_sup f) . x = lim_sup (R_EAL (f # x)) by Th13;
hence  ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) by A1, A5, A3, Th14; ::_thesis: verum
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 number 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
let X be non empty set ; ::_thesis: 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 number 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))
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being real number 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))
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for F being SetSequence of S
for r being real number 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))
let F be SetSequence of S; ::_thesis: for r being real number 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))
let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) implies union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) )
set E = dom (f . 0);
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ; ::_thesis: union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))
now__::_thesis:_for_x_being_set_st_x_in_(dom_(f_._0))_/\_(great_dom_((sup_f),r))_holds_
x_in_union_(rng_F)
let x be set ; ::_thesis: ( x in (dom (f . 0)) /\ (great_dom ((sup f),r)) implies x in union (rng F) )
assume A2: x in (dom (f . 0)) /\ (great_dom ((sup f),r)) ; ::_thesis: x in union (rng F)
then reconsider z = x as Element of X ;
A3: x in dom (f . 0) by A2, XBOOLE_0:def_4;
 x in great_dom ((sup f),r) by A2, XBOOLE_0:def_4;
then A4: r < (sup f) . z by MESFUNC1:def_13;
 ex n being Element of NAT st r < (f # z) . n
proof
assume A5: for n being Element of NAT holds (f # z) . n <= r ; ::_thesis: contradiction
 for p being ext-real number st p in rng (R_EAL (f # z)) holds
p <= r
proof
let p be ext-real number ; ::_thesis: ( p in rng (R_EAL (f # z)) implies p <= r )
assume  p in rng (R_EAL (f # z)) ; ::_thesis: p <= r
then  ex n being set st
( n in NAT & (R_EAL (f # z)) . n = p ) by FUNCT_2:11;
hence  p <= r by A5; ::_thesis: verum
end;
then  r is UpperBound of rng (R_EAL (f # z)) by XXREAL_2:def_1;
then A6: sup (rng (R_EAL (f # z))) <= r by XXREAL_2:def_3;
 x in dom (sup f) by A3, MESFUNC8:def_4;
hence  contradiction by A4, A6, Th3; ::_thesis: verum
end;
then consider n being Element of NAT  such that
A7: r < (f # z) . n ;
A8: x in dom (f . n) by A3, MESFUNC8:def_2;
 r < (f . n) . z by A7, SEQFUNC:def_10;
then A9: x in great_dom ((f . n),r) by A8, MESFUNC1:def_13;
A10: F . n in rng F by FUNCT_2:4;
 F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) by A1;
then  x in F . n by A3, A9, XBOOLE_0:def_4;
hence  x in union (rng F) by A10, TARSKI:def_4; ::_thesis: verum
end;
then A11: (dom (f . 0)) /\ (great_dom ((sup f),r)) c= union (rng F) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_union_(rng_F)_holds_
x_in_(dom_(f_._0))_/\_(great_dom_((sup_f),r))
let x be set ; ::_thesis: ( x in union (rng F) implies x in (dom (f . 0)) /\ (great_dom ((sup f),r)) )
assume  x in union (rng F) ; ::_thesis: x in (dom (f . 0)) /\ (great_dom ((sup f),r))
then consider y being set  such that
A12: x in y and
A13: y in rng F by TARSKI:def_4;
reconsider z = x as Element of X by A12, A13;
consider n being set  such that
A14: n in dom F and
A15: y = F . n by A13, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A14;
A16: F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) by A1;
then  x in great_dom ((f . n),r) by A12, A15, XBOOLE_0:def_4;
then A17: r < (f . n) . z by MESFUNC1:def_13;
 f # z = (R_EAL f) # z by Th1;
then  (f . n) . z = ((R_EAL f) # z) . n by SEQFUNC:def_10;
then A18: (f . n) . z <= sup (rng ((R_EAL f) # z)) by FUNCT_2:4, XXREAL_2:4;
A19: x in dom (f . 0) by A12, A15, A16, XBOOLE_0:def_4;
then A20: x in dom (sup f) by MESFUNC8:def_4;
then  (sup f) . z = sup ((R_EAL f) # z) by MESFUNC8:def_4;
then  r < (sup f) . z by A17, A18, XXREAL_0:2;
then  x in great_dom ((sup f),r) by A20, MESFUNC1:def_13;
hence  x in (dom (f . 0)) /\ (great_dom ((sup f),r)) by A19, XBOOLE_0:def_4; ::_thesis: verum
end;
then  union (rng F) c= (dom (f . 0)) /\ (great_dom ((sup f),r)) by TARSKI:def_3;
hence  union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) by A11, XBOOLE_0:def_10; ::_thesis: verum
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 number 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
let X be non empty set ; ::_thesis: 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 number 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))
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being real number 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))
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for F being SetSequence of S
for r being real number 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))
let F be SetSequence of S; ::_thesis: for r being real number 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))
let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) implies meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) )
set E = dom (f . 0);
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ; ::_thesis: meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_F)_holds_
x_in_(dom_(f_._0))_/\_(great_eq_dom_((inf_f),r))
let x be set ; ::_thesis: ( x in meet (rng F) implies x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) )
assume A2: x in meet (rng F) ; ::_thesis: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
then reconsider z = x as Element of X ;
A3: F . 0 = (dom (f . 0)) /\ (great_eq_dom ((f . 0),r)) by A1;
 F . 0 in rng F by FUNCT_2:4;
then  x in F . 0 by A2, SETFAM_1:def_1;
then A4: x in dom (f . 0) by A3, XBOOLE_0:def_4;
then A5: x in dom (inf f) by MESFUNC8:def_3;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_r_<=_(R_EAL_(f_#_z))_._n
let n be Element of NAT ; ::_thesis: r <= (R_EAL (f # z)) . n
 F . n in rng F by FUNCT_2:4;
then A7: z in F . n by A2, SETFAM_1:def_1;
 F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) by A1;
then  x in great_eq_dom ((f . n),r) by A7, XBOOLE_0:def_4;
then  r <= (f . n) . z by MESFUNC1:def_14;
hence  r <= (R_EAL (f # z)) . n by SEQFUNC:def_10; ::_thesis: verum
end;
 for p being ext-real number st p in rng (R_EAL (f # z)) holds
r <= p
proof
let p be ext-real number ; ::_thesis: ( p in rng (R_EAL (f # z)) implies r <= p )
assume  p in rng (R_EAL (f # z)) ; ::_thesis: r <= p
then  ex n being set st
( n in NAT & (R_EAL (f # z)) . n = p ) by FUNCT_2:11;
hence  r <= p by A6; ::_thesis: verum
end;
then  r is LowerBound of rng (R_EAL (f # z)) by XXREAL_2:def_2;
then  r <= inf (rng (R_EAL (f # z))) by XXREAL_2:def_4;
then  r <= (inf f) . x by A5, Th2;
then  x in great_eq_dom ((inf f),r) by A5, MESFUNC1:def_14;
hence  x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
then A8: meet (rng F) c= (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_(dom_(f_._0))_/\_(great_eq_dom_((inf_f),r))_holds_
x_in_meet_(rng_F)
let x be set ; ::_thesis: ( x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) implies x in meet (rng F) )
assume A9: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) ; ::_thesis: x in meet (rng F)
then reconsider z = x as Element of X ;
A10: x in dom (f . 0) by A9, XBOOLE_0:def_4;
 x in great_eq_dom ((inf f),r) by A9, XBOOLE_0:def_4;
then A11: r <= (inf f) . z by MESFUNC1:def_14;
now__::_thesis:_for_y_being_set_st_y_in_rng_F_holds_
x_in_y
let y be set ; ::_thesis: ( y in rng F implies x in y )
assume  y in rng F ; ::_thesis: x in y
then consider n being set  such that
A12: n in NAT and
A13: y = F . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A12;
A14: x in dom (f . n) by A10, MESFUNC8:def_2;
 x in dom (inf f) by A10, MESFUNC8:def_3;
then A15: (inf f) . z = inf (rng (R_EAL (f # z))) by Th2;
 (f . n) . z = (R_EAL (f # z)) . n by SEQFUNC:def_10;
then  (f . n) . z >= inf (rng (R_EAL (f # z))) by FUNCT_2:4, XXREAL_2:3;
then  r <= (f . n) . z by A11, A15, XXREAL_0:2;
then A16: x in great_eq_dom ((f . n),r) by A14, MESFUNC1:def_14;
 F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) by A1;
hence  x in y by A10, A13, A16, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum
end;
then  (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) c= meet (rng F) by TARSKI:def_3;
hence  meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by A8, XBOOLE_0:def_10; ::_thesis: verum
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_measurable_on E ) holds
lim_sup f is_measurable_on E
proof
let X be non empty set ; ::_thesis: 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_measurable_on E ) holds
lim_sup f is_measurable_on E
let S be SigmaField of X; ::_thesis: 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_measurable_on E ) holds
lim_sup f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies lim_sup f is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: lim_sup f is_measurable_on E
 for n being Nat holds (R_EAL f) . n is_measurable_on E by A2, Th7;
hence  lim_sup f is_measurable_on E by A1, MESFUNC8:23; ::_thesis: verum
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_measurable_on E ) holds
lim_inf f is_measurable_on E
proof
let X be non empty set ; ::_thesis: 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_measurable_on E ) holds
lim_inf f is_measurable_on E
let S be SigmaField of X; ::_thesis: 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_measurable_on E ) holds
lim_inf f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_inf f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies lim_inf f is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: lim_inf f is_measurable_on E
 for n being Nat holds (R_EAL f) . n is_measurable_on E by A2, Th7;
hence  lim_inf f is_measurable_on E by A1, MESFUNC8:24; ::_thesis: verum
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
(superior_realsequence f) # x is bounded_below
proof
let X be non empty set ; ::_thesis: 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
(superior_realsequence f) # x is bounded_below
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (f . 0) & f # x is convergent holds
(superior_realsequence f) # x is bounded_below
let x be Element of X; ::_thesis: ( x in dom (f . 0) & f # x is convergent implies (superior_realsequence f) # x is bounded_below )
assume A1: x in dom (f . 0) ; ::_thesis: ( not f # x is convergent or (superior_realsequence f) # x is bounded_below )
assume  f # x is convergent ; ::_thesis: (superior_realsequence f) # x is bounded_below
then A2: f # x is bounded ;
then  superior_realsequence (R_EAL (f # x)) = superior_realsequence (f # x) by RINFSUP2:9;
then A3: (superior_realsequence f) # x = superior_realsequence (f # x) by A1, Th11;
 superior_realsequence (f # x) is bounded by A2, RINFSUP1:56;
hence  (superior_realsequence f) # x is bounded_below by A3, RINFSUP2:13; ::_thesis: verum
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_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
proof
let X be non empty set ; ::_thesis: 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_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let S be SigmaField of X; ::_thesis: 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_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) implies lim f is_measurable_on E )
assume A1: dom (f . 0) = E ; ::_thesis: ( ex n being Nat st not f . n is_measurable_on E or ex x being Element of X st
( x in E & not f # x is convergent ) or lim f is_measurable_on E )
then A2: dom (lim f) = E by MESFUNC8:def_9;
assume  for n being Nat holds f . n is_measurable_on E ; ::_thesis: ( ex x being Element of X st
( x in E & not f # x is convergent ) or lim f is_measurable_on E )
then A3: lim_sup f is_measurable_on E by A1, Th18;
assume A4: for x being Element of X st x in E holds
f # x is convergent ; ::_thesis: lim f is_measurable_on E
A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_f)_holds_
(lim_f)_._x_=_(lim_sup_f)_._x
let x be Element of X; ::_thesis: ( x in dom (lim f) implies (lim f) . x = (lim_sup f) . x )
assume A6: x in dom (lim f) ; ::_thesis: (lim f) . x = (lim_sup f) . x
then  f # x is convergent by A2, A4;
hence  (lim f) . x = (lim_sup f) . x by A6, Th15; ::_thesis: verum
end;
 dom (lim_sup f) = E by A1, MESFUNC8:def_8;
hence  lim f is_measurable_on E by A2, A3, A5, PARTFUN1:5; ::_thesis: verum
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_measurable_on E ) & 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_measurable_on E
proof
let X be non empty set ; ::_thesis: 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_measurable_on E ) & 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_measurable_on E
let S be SigmaField of X; ::_thesis: 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_measurable_on E ) & 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_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: 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_measurable_on E ) & 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_measurable_on E
let g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & 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_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) implies g is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E and
A3: dom g = E and
A4: for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ; ::_thesis: g is_measurable_on E
A5: dom (lim f) = E by A1, MESFUNC8:def_9;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_f)_holds_
g_._x_=_(lim_f)_._x
let x be Element of X; ::_thesis: ( x in dom (lim f) implies g . x = (lim f) . x )
assume A6: x in dom (lim f) ; ::_thesis: g . x = (lim f) . x
then  x in E by A1, MESFUNC8:def_9;
then  f # x is convergent by A4;
then  lim (f # x) = lim (R_EAL (f # x)) by RINFSUP2:14;
then  g . x = lim (R_EAL (f # x)) by A4, A5, A6;
hence  g . x = (lim f) . x by A6, Th14; ::_thesis: verum
end;
then A7: g = lim f by A3, A5, PARTFUN1:5;
 for x being Element of X st x in E holds
f # x is convergent by A4;
hence  g is_measurable_on E by A1, A2, A7, Th21; ::_thesis: verum
end;

begin

definition
let X be non empty set ;
let H be Functional_Sequence of X,COMPLEX;
let x be Element of X;
funcH # 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
defpred S1[ Element of NAT , set ] means $2 = (H . $1) . x;
A1: for n being Element of NAT ex y being Element of COMPLEX st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of COMPLEX st S1[n,y]
 (H . n) . x in COMPLEX by XCMPLX_0:def_2;
hence  ex y being Element of COMPLEX st S1[n,y] ; ::_thesis: verum
end;
consider f being Function of NAT,COMPLEX such that
A2: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1);
take  f ; ::_thesis: for n being Nat holds f . n = (H . n) . x
let n be Nat; ::_thesis: f . n = (H . n) . x
 n in NAT by ORDINAL1:def_12;
hence  f . n = (H . n) . x by A2; ::_thesis: verum
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
let S1, S2 be Complex_Sequence; ::_thesis: ( ( for n being Nat holds S1 . n = (H . n) . x ) & ( for n being Nat holds S2 . n = (H . n) . x ) implies S1 = S2 )
assume that
A3: for n being Nat holds S1 . n = (H . n) . x and
A4: for n being Nat holds S2 . n = (H . n) . x ; ::_thesis: S1 = S2
now__::_thesis:_for_n_being_Element_of_NAT_holds_S1_._n_=_S2_._n
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
 S1 . n = (H . n) . x by A3;
hence  S1 . n = S2 . n by A4; ::_thesis: verum
end;
hence  S1 = S2 by FUNCT_2:63; ::_thesis: verum
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
defpred S1[ set ] means $1 in dom (f . 0);
deffunc H1( Element of X) ->  Element of COMPLEX = lim (f # $1);
consider g being PartFunc of X,COMPLEX such that
A1: ( ( for x being Element of X holds
( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take  g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim (f # x) ) )
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_lim_(f_#_x)
let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim (f # x) )
assume A3: x in dom g ; ::_thesis: g . x = lim (f # x)
then  g /. x = lim (f # x) by A1;
hence  g . x = lim (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum
end;
 for x being set holds
( x in dom g iff x in dom (f . 0) ) by A1;
hence  ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum
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
let g, h be PartFunc of X,COMPLEX; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds
h . x = lim (f # x) ) implies g = h )
assume that
A4: dom g = dom (f . 0) and
A5: for x being Element of X st x in dom g holds
g . x = lim (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st
( x in dom h & not h . x = lim (f # x) ) or g = h )
assume that
A6: dom h = dom (f . 0) and
A7: for x being Element of X st x in dom h holds
h . x = lim (f # x) ; ::_thesis: g = h
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_h_._x
let x be Element of X; ::_thesis: ( x in dom g implies g . x = h . x )
assume A8: x in dom g ; ::_thesis: g . x = h . x
then  g . x = lim (f # x) by A5;
hence  g . x = h . x by A4, A6, A7, A8; ::_thesis: verum
end;
hence  g = h by A4, A6, PARTFUN1:5; ::_thesis: verum
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
defpred S1[ Element of NAT , Function] means ( dom $2 = dom (f . $1) & ( for x being Element of X st x in dom $2 holds
$2 . x = (Re (f # x)) . $1 ) );
A1: for n being Element of NAT ex y being Element of PFuncs (X,REAL) st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of PFuncs (X,REAL) st S1[n,y]
deffunc H1( Element of X) ->  Element of REAL = (Re (f # $1)) . n;
defpred S2[ set ] means $1 in dom (f . n);
consider g being PartFunc of X,REAL such that
A2: ( ( for x being Element of X holds
( x in dom g iff S2[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take  g ; ::_thesis: ( g is Element of PFuncs (X,REAL) & S1[n,g] )
A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_(Re_(f_#_x))_._n
let x be Element of X; ::_thesis: ( x in dom g implies g . x = (Re (f # x)) . n )
assume A4: x in dom g ; ::_thesis: g . x = (Re (f # x)) . n
then  g /. x = (Re (f # x)) . n by A2;
hence  g . x = (Re (f # x)) . n by A4, PARTFUN1:def_6; ::_thesis: verum
end;
 for x being set holds
( x in dom g iff x in dom (f . n) ) by A2;
hence  ( g is Element of PFuncs (X,REAL) & S1[n,g] ) by A3, PARTFUN1:45, TARSKI:1; ::_thesis: verum
end;
consider g being Function of NAT,(PFuncs (X,REAL)) such that
A5: for n being Element of NAT holds S1[n,g . n] from FUNCT_2:sch_3(A1);
reconsider g = g as Functional_Sequence of X,REAL ;
take  g ; ::_thesis: for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) )
thus  for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) ) ::_thesis: verum
proof
let n be Nat; ::_thesis: ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) )
 n in NAT by ORDINAL1:def_12;
hence  ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) ) by A5; ::_thesis: verum
end;
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
let g, h be Functional_Sequence of X,REAL; ::_thesis: ( ( for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (Re (f # x)) . n ) ) ) implies g = h )
assume A6: for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) ) ; ::_thesis: ( ex n being Nat st
( dom (h . n) = dom (f . n) implies ex x being Element of X st
( x in dom (h . n) & not (h . n) . x = (Re (f # x)) . n ) ) or g = h )
assume A7: for n being Nat holds
( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (Re (f # x)) . n ) ) ; ::_thesis: g = h
now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_=_h_._n
let n be Element of NAT ; ::_thesis: g . n = h . n
A8: dom (g . n) = dom (f . n) by A6
.= dom (h . n) by A7 ;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(g_._n)_holds_
(g_._n)_._x_=_(h_._n)_._x
let x be Element of X; ::_thesis: ( x in dom (g . n) implies (g . n) . x = (h . n) . x )
assume A9: x in dom (g . n) ; ::_thesis: (g . n) . x = (h . n) . x
then  (g . n) . x = (Re (f # x)) . n by A6;
hence  (g . n) . x = (h . n) . x by A7, A8, A9; ::_thesis: verum
end;
hence  g . n = h . n by A8, PARTFUN1:5; ::_thesis: verum
end;
hence  g = h by FUNCT_2:63; ::_thesis: verum
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;
cluster Re f ->  with_the_same_dom ;
correctness
coherence
Re f is with_the_same_dom ;
proof
now__::_thesis:_for_k,_l_being_Nat_holds_dom_((Re_f)_._k)_=_dom_((Re_f)_._l)
let k, l be Nat; ::_thesis: dom ((Re f) . k) = dom ((Re f) . l)
 dom ((Re f) . k) = dom (f . k) by Def11;
then  dom ((Re f) . k) = dom (f . l) by MESFUNC8:def_2;
hence  dom ((Re f) . k) = dom ((Re f) . l) by Def11; ::_thesis: verum
end;
hence  Re f is with_the_same_dom by MESFUNC8:def_2; ::_thesis: verum
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
defpred S1[ Element of NAT , Function] means ( dom $2 = dom (f . $1) & ( for x being Element of X st x in dom $2 holds
$2 . x = (Im (f # x)) . $1 ) );
A1: for n being Element of NAT ex y being Element of PFuncs (X,REAL) st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of PFuncs (X,REAL) st S1[n,y]
deffunc H1( Element of X) ->  Element of REAL = (Im (f # $1)) . n;
defpred S2[ set ] means $1 in dom (f . n);
consider g being PartFunc of X,REAL such that
A2: ( ( for x being Element of X holds
( x in dom g iff S2[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take  g ; ::_thesis: ( g is Element of PFuncs (X,REAL) & S1[n,g] )
A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_(Im_(f_#_x))_._n
let x be Element of X; ::_thesis: ( x in dom g implies g . x = (Im (f # x)) . n )
assume A4: x in dom g ; ::_thesis: g . x = (Im (f # x)) . n
then  g /. x = (Im (f # x)) . n by A2;
hence  g . x = (Im (f # x)) . n by A4, PARTFUN1:def_6; ::_thesis: verum
end;
 for x being set holds
( x in dom g iff x in dom (f . n) ) by A2;
hence  ( g is Element of PFuncs (X,REAL) & S1[n,g] ) by A3, PARTFUN1:45, TARSKI:1; ::_thesis: verum
end;
consider g being Function of NAT,(PFuncs (X,REAL)) such that
A5: for n being Element of NAT holds S1[n,g . n] from FUNCT_2:sch_3(A1);
reconsider g = g as Functional_Sequence of X,REAL ;
take  g ; ::_thesis: for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) )
thus  for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) ) ::_thesis: verum
proof
let n be Nat; ::_thesis: ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) )
 n in NAT by ORDINAL1:def_12;
hence  ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) ) by A5; ::_thesis: verum
end;
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
let g, h be Functional_Sequence of X,REAL; ::_thesis: ( ( for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (Im (f # x)) . n ) ) ) implies g = h )
assume A6: for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) ) ; ::_thesis: ( ex n being Nat st
( dom (h . n) = dom (f . n) implies ex x being Element of X st
( x in dom (h . n) & not (h . n) . x = (Im (f # x)) . n ) ) or g = h )
assume A7: for n being Nat holds
( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (Im (f # x)) . n ) ) ; ::_thesis: g = h
now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_=_h_._n
let n be Element of NAT ; ::_thesis: g . n = h . n
A8: dom (g . n) = dom (f . n) by A6
.= dom (h . n) by A7 ;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(g_._n)_holds_
(g_._n)_._x_=_(h_._n)_._x
let x be Element of X; ::_thesis: ( x in dom (g . n) implies (g . n) . x = (h . n) . x )
assume A9: x in dom (g . n) ; ::_thesis: (g . n) . x = (h . n) . x
then  (g . n) . x = (Im (f # x)) . n by A6;
hence  (g . n) . x = (h . n) . x by A7, A8, A9; ::_thesis: verum
end;
hence  g . n = h . n by A8, PARTFUN1:5; ::_thesis: verum
end;
hence  g = h by FUNCT_2:63; ::_thesis: verum
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;
cluster Im f ->  with_the_same_dom ;
correctness
coherence
Im f is with_the_same_dom ;
proof
now__::_thesis:_for_k,_l_being_Nat_holds_dom_((Im_f)_._k)_=_dom_((Im_f)_._l)
let k, l be Nat; ::_thesis: dom ((Im f) . k) = dom ((Im f) . l)
 dom ((Im f) . k) = dom (f . k) by Def12;
then  dom ((Im f) . k) = dom (f . l) by MESFUNC8:def_2;
hence  dom ((Im f) . k) = dom ((Im f) . l) by Def12; ::_thesis: verum
end;
hence  Im f is with_the_same_dom by MESFUNC8:def_2; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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) )
let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: 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) )
let x be Element of X; ::_thesis: ( x in dom (f . 0) implies ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) )
set F = Re f;
set G = Im f;
assume A1: x in dom (f . 0) ; ::_thesis: ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_((Re_f)_#_x)_._n_=_(Re_(f_#_x))_._n_&_((Im_f)_#_x)_._n_=_(Im_(f_#_x))_._n_)
let n be Element of NAT ; ::_thesis: ( ((Re f) # x) . n = (Re (f # x)) . n & ((Im f) # x) . n = (Im (f # x)) . n )
 dom ((Re f) . n) = dom (f . n) by Def11;
then A2: dom ((Re f) . n) = dom (f . 0) by MESFUNC8:def_2;
 dom ((Im f) . n) = dom (f . n) by Def12;
then A3: dom ((Im f) . n) = dom (f . 0) by MESFUNC8:def_2;
 ( ((Re f) # x) . n = ((Re f) . n) . x & ((Im f) # x) . n = ((Im f) . n) . x ) by SEQFUNC:def_10;
hence  ( ((Re f) # x) . n = (Re (f # x)) . n & ((Im f) # x) . n = (Im (f # x)) . n ) by A1, A2, A3, Def11, Def12; ::_thesis: verum
end;
hence  ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) by FUNCT_2:63; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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) )
let f be Functional_Sequence of X,COMPLEX; ::_thesis: for n being Nat holds
( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
let n be Nat; ::_thesis: ( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
A1: n in NAT by ORDINAL1:def_12;
 dom ((Re f) . n) = dom (f . n) by Def11;
then A2: dom ((Re f) . n) = dom (Re (f . n)) by COMSEQ_3:def_3;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((Re_f)_._n)_holds_
((Re_f)_._n)_._x_=_(Re_(f_._n))_._x
let x be Element of X; ::_thesis: ( x in dom ((Re f) . n) implies ((Re f) . n) . x = (Re (f . n)) . x )
assume A3: x in dom ((Re f) . n) ; ::_thesis: ((Re f) . n) . x = (Re (f . n)) . x
then  (Re (f . n)) . x = Re ((f . n) . x) by A2, COMSEQ_3:def_3;
then A4: (Re (f . n)) . x = Re ((f # x) . n) by Def9;
 ((Re f) . n) . x = (Re (f # x)) . n by A3, Def11;
hence  ((Re f) . n) . x = (Re (f . n)) . x by A1, A4, COMSEQ_3:def_5; ::_thesis: verum
end;
hence  (Re f) . n = Re (f . n) by A2, PARTFUN1:5; ::_thesis: (Im f) . n = Im (f . n)
 dom ((Im f) . n) = dom (f . n) by Def12;
then A5: dom ((Im f) . n) = dom (Im (f . n)) by COMSEQ_3:def_4;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((Im_f)_._n)_holds_
((Im_f)_._n)_._x_=_(Im_(f_._n))_._x
let x be Element of X; ::_thesis: ( x in dom ((Im f) . n) implies ((Im f) . n) . x = (Im (f . n)) . x )
assume A6: x in dom ((Im f) . n) ; ::_thesis: ((Im f) . n) . x = (Im (f . n)) . x
then  (Im (f . n)) . x = Im ((f . n) . x) by A5, COMSEQ_3:def_4;
then A7: (Im (f . n)) . x = Im ((f # x) . n) by Def9;
 ((Im f) . n) . x = (Im (f # x)) . n by A6, Def12;
hence  ((Im f) . n) . x = (Im (f . n)) . x by A1, A7, COMSEQ_3:def_6; ::_thesis: verum
end;
hence  (Im f) . n = Im (f . n) by A5, PARTFUN1:5; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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) )
let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: ( ( for x being Element of X st x in dom (f . 0) holds
f # x is convergent ) implies ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) ) )
 dom (lim (Re f)) = dom ((Re f) . 0) by MESFUNC8:def_9;
then A1: dom (lim (Re f)) = dom (f . 0) by Def11;
A2: dom (Re (lim f)) = dom (lim f) by COMSEQ_3:def_3;
then A3: dom (lim (Re f)) = dom (Re (lim f)) by A1, Def10;
assume A4: for x being Element of X st x in dom (f . 0) holds
f # x is convergent ; ::_thesis: ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )
A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_(Re_f))_holds_
(lim_(Re_f))_._x_=_(Re_(lim_f))_._x
let x be Element of X; ::_thesis: ( x in dom (lim (Re f)) implies (lim (Re f)) . x = (Re (lim f)) . x )
assume A6: x in dom (lim (Re f)) ; ::_thesis: (lim (Re f)) . x = (Re (lim f)) . x
then A7: f # x is convergent by A4, A1;
then  Re (f # x) is convergent ;
then A8: (Re f) # x is convergent by A1, A6, Th23;
(lim (Re f)) . x = lim (R_EAL ((Re f) # x)) by A6, Th14
.= lim ((Re f) # x) by A8, RINFSUP2:14 ;
then  (lim (Re f)) . x = lim (Re (f # x)) by A1, A6, Th23;
then A9: (lim (Re f)) . x = Re (lim (f # x)) by A7, COMSEQ_3:41;
 (Re (lim f)) . x = Re ((lim f) . x) by A3, A6, COMSEQ_3:def_3;
hence  (lim (Re f)) . x = (Re (lim f)) . x by A2, A3, A6, A9, Def10; ::_thesis: verum
end;
 Re (lim f) is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7;
hence  lim (Re f) = Re (lim f) by A3, A5, PARTFUN1:5; ::_thesis: lim (Im f) = Im (lim f)
 dom (lim (Im f)) = dom ((Im f) . 0) by MESFUNC8:def_9;
then A10: dom (lim (Im f)) = dom (f . 0) by Def12;
A11: dom (Im (lim f)) = dom (lim f) by COMSEQ_3:def_4;
then A12: dom (lim (Im f)) = dom (Im (lim f)) by A10, Def10;
A13: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_(Im_f))_holds_
(lim_(Im_f))_._x_=_(Im_(lim_f))_._x
let x be Element of X; ::_thesis: ( x in dom (lim (Im f)) implies (lim (Im f)) . x = (Im (lim f)) . x )
assume A14: x in dom (lim (Im f)) ; ::_thesis: (lim (Im f)) . x = (Im (lim f)) . x
then A15: f # x is convergent by A4, A10;
then  Im (f # x) is convergent ;
then A16: (Im f) # x is convergent by A10, A14, Th23;
(lim (Im f)) . x = lim (R_EAL ((Im f) # x)) by A14, Th14
.= lim ((Im f) # x) by A16, RINFSUP2:14 ;
then  (lim (Im f)) . x = lim (Im (f # x)) by A10, A14, Th23;
then A17: (lim (Im f)) . x = Im (lim (f # x)) by A15, COMSEQ_3:41;
 (Im (lim f)) . x = Im ((lim f) . x) by A12, A14, COMSEQ_3:def_4;
hence  (lim (Im f)) . x = (Im (lim f)) . x by A11, A12, A14, A17, Def10; ::_thesis: verum
end;
 Im (lim f) is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7;
hence  lim (Im f) = Im (lim f) by A12, A13, PARTFUN1:5; ::_thesis: verum
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_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
proof
let X be non empty set ; ::_thesis: 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_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let S be SigmaField of X; ::_thesis: 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_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) implies lim f is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E and
A3: for x being Element of X st x in E holds
f # x is convergent ; ::_thesis: lim f is_measurable_on E
A4: lim (Im f) = R_EAL (Im (lim f)) by A1, A3, Th25;
A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(Im_f)_#_x_is_convergent
let x be Element of X; ::_thesis: ( x in E implies (Im f) # x is convergent )
assume A6: x in E ; ::_thesis: (Im f) # x is convergent
then  f # x is convergent by A3;
then  Im (f # x) is convergent ;
hence  (Im f) # x is convergent by A1, A6, Th23; ::_thesis: verum
end;
A7: now__::_thesis:_for_n_being_Nat_holds_(Im_f)_._n_is_measurable_on_E
let n be Nat; ::_thesis: (Im f) . n is_measurable_on E
 f . n is_measurable_on E by A2;
then  Im (f . n) is_measurable_on E by MESFUN6C:def_1;
hence  (Im f) . n is_measurable_on E by Th24; ::_thesis: verum
end;
 dom ((Im f) . 0) = E by A1, Def12;
then  lim (Im f) is_measurable_on E by A7, A5, Th21;
then A8: Im (lim f) is_measurable_on E by A4, MESFUNC6:def_1;
A9: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(Re_f)_#_x_is_convergent
let x be Element of X; ::_thesis: ( x in E implies (Re f) # x is convergent )
assume A10: x in E ; ::_thesis: (Re f) # x is convergent
then  f # x is convergent by A3;
then  Re (f # x) is convergent ;
hence  (Re f) # x is convergent by A1, A10, Th23; ::_thesis: verum
end;
A11: now__::_thesis:_for_n_being_Nat_holds_(Re_f)_._n_is_measurable_on_E
let n be Nat; ::_thesis: (Re f) . n is_measurable_on E
 f . n is_measurable_on E by A2;
then  Re (f . n) is_measurable_on E by MESFUN6C:def_1;
hence  (Re f) . n is_measurable_on E by Th24; ::_thesis: verum
end;
A12: lim (Re f) = R_EAL (Re (lim f)) by A1, A3, Th25;
 dom ((Re f) . 0) = E by A1, Def11;
then  lim (Re f) is_measurable_on E by A11, A9, Th21;
then  Re (lim f) is_measurable_on E by A12, MESFUNC6:def_1;
hence  lim f is_measurable_on E by A8, MESFUN6C:def_1; ::_thesis: verum
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_measurable_on E ) & 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_measurable_on E
proof
let X be non empty set ; ::_thesis: 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_measurable_on E ) & 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_measurable_on E
let S be SigmaField of X; ::_thesis: 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_measurable_on E ) & 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_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: 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_measurable_on E ) & 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_measurable_on E
let g be PartFunc of X,COMPLEX; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & 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_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) implies g is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E and
A3: dom g = E and
A4: for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ; ::_thesis: g is_measurable_on E
A5: now__::_thesis:_for_n_being_Nat_holds_(Im_f)_._n_is_measurable_on_E
let n be Nat; ::_thesis: (Im f) . n is_measurable_on E
 f . n is_measurable_on E by A2;
then  Im (f . n) is_measurable_on E by MESFUN6C:def_1;
hence  (Im f) . n is_measurable_on E by Th24; ::_thesis: verum
end;
A6: dom (Im g) = E by A3, COMSEQ_3:def_4;
A7: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(_(Im_f)_#_x_is_convergent_&_(Im_g)_._x_=_lim_((Im_f)_#_x)_)
let x be Element of X; ::_thesis: ( x in E implies ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) ) )
assume A8: x in E ; ::_thesis: ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) )
then A9: f # x is convergent by A4;
then  Im (f # x) is convergent ;
hence  (Im f) # x is convergent by A1, A8, Th23; ::_thesis: (Im g) . x = lim ((Im f) # x)
 g . x = lim (f # x) by A4, A8;
then  Im (g . x) = lim (Im (f # x)) by A9, COMSEQ_3:41;
then  Im (g . x) = lim ((Im f) # x) by A1, A8, Th23;
hence  (Im g) . x = lim ((Im f) # x) by A6, A8, COMSEQ_3:def_4; ::_thesis: verum
end;
 dom ((Im f) . 0) = E by A1, Def12;
then  R_EAL (Im g) is_measurable_on E by A5, A6, A7, Th22;
then A10: Im g is_measurable_on E by MESFUNC6:def_1;
A11: now__::_thesis:_for_n_being_Nat_holds_(Re_f)_._n_is_measurable_on_E
let n be Nat; ::_thesis: (Re f) . n is_measurable_on E
 f . n is_measurable_on E by A2;
then  Re (f . n) is_measurable_on E by MESFUN6C:def_1;
hence  (Re f) . n is_measurable_on E by Th24; ::_thesis: verum
end;
A12: dom (Re g) = E by A3, COMSEQ_3:def_3;
A13: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(_(Re_f)_#_x_is_convergent_&_(Re_g)_._x_=_lim_((Re_f)_#_x)_)
let x be Element of X; ::_thesis: ( x in E implies ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) ) )
assume A14: x in E ; ::_thesis: ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) )
then A15: f # x is convergent by A4;
then  Re (f # x) is convergent ;
hence  (Re f) # x is convergent by A1, A14, Th23; ::_thesis: (Re g) . x = lim ((Re f) # x)
 g . x = lim (f # x) by A4, A14;
then  Re (g . x) = lim (Re (f # x)) by A15, COMSEQ_3:41;
then  Re (g . x) = lim ((Re f) # x) by A1, A14, Th23;
hence  (Re g) . x = lim ((Re f) # x) by A12, A14, COMSEQ_3:def_3; ::_thesis: verum
end;
 dom ((Re f) . 0) = E by A1, Def11;
then  R_EAL (Re g) is_measurable_on E by A11, A12, A13, Th22;
then  Re g is_measurable_on E by MESFUNC6:def_1;
hence  g is_measurable_on E by A10, MESFUN6C:def_1; ::_thesis: verum
end;

begin

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
let X be non empty set ; ::_thesis: for Y being set
for f being PartFunc of X,COMPLEX
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let Y be set ; ::_thesis: for f being PartFunc of X,COMPLEX
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let f be PartFunc of X,COMPLEX; ::_thesis: for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let r be Real; ::_thesis: (r (#) f) | Y = r (#) (f | Y)
A1: dom ((r (#) f) | Y) = (dom (r (#) f)) /\ Y by RELAT_1:61;
then  dom ((r (#) f) | Y) = (dom f) /\ Y by VALUED_1:def_5;
then A2: dom ((r (#) f) | Y) = dom (f | Y) by RELAT_1:61;
then A3: dom ((r (#) f) | Y) = dom (r (#) (f | Y)) by VALUED_1:def_5;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((r_(#)_f)_|_Y)_holds_
((r_(#)_f)_|_Y)_._x_=_(r_(#)_(f_|_Y))_._x
let x be Element of X; ::_thesis: ( x in dom ((r (#) f) | Y) implies ((r (#) f) | Y) . x = (r (#) (f | Y)) . x )
assume A4: x in dom ((r (#) f) | Y) ; ::_thesis: ((r (#) f) | Y) . x = (r (#) (f | Y)) . x
then A5: x in dom (r (#) f) by A1, XBOOLE_0:def_4;
thus ((r (#) f) | Y) . x = (r (#) f) . x by A4, FUNCT_1:47
.= r * (f . x) by A5, VALUED_1:def_5
.= r * ((f | Y) . x) by A2, A4, FUNCT_1:47
.= (r (#) (f | Y)) . x by A3, A4, VALUED_1:def_5 ; ::_thesis: verum
end;
hence  (r (#) f) | Y = r (#) (f | Y) by A3, PARTFUN1:5; ::_thesis: verum
end;

Lm1:  for X being non empty set
for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative
let f be PartFunc of X,COMPLEX; ::_thesis: |.f.| is nonnegative
now__::_thesis:_for_x_being_set_st_x_in_dom_|.f.|_holds_
0_<=_|.f.|_._x
let x be set ; ::_thesis: ( x in dom |.f.| implies 0 <= |.f.| . x )
assume  x in dom |.f.| ; ::_thesis: 0 <= |.f.| . x
then  |.f.| . x = |.(f . x).| by VALUED_1:def_11;
hence  0 <= |.f.| . x by COMPLEX1:46; ::_thesis: verum
end;
hence  |.f.| is nonnegative by MESFUNC6:52; ::_thesis: verum
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 number
for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for k being real number
for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for k being real number
for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
let f be PartFunc of X,COMPLEX; ::_thesis: for k being real number
for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
let k be real number ; ::_thesis: for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
let E be Element of S; ::_thesis: ( 0 <= k & E c= dom f & f is_measurable_on E implies |.f.| to_power k is_measurable_on E )
assume that
A1: 0 <= k and
A2: E c= dom f and
A3: f is_measurable_on E ; ::_thesis: |.f.| to_power k is_measurable_on E
A4: |.f.| is nonnegative by Lm1;
 E c= dom |.f.| by A2, VALUED_1:def_11;
hence  |.f.| to_power k is_measurable_on E by A1, A2, A3, A4, MESFUN6C:29, MESFUN6C:30; ::_thesis: verum
end;

theorem Th30: :: MESFUN7C:30
for X being non empty set
for f, g being PartFunc of X,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)
let f, g be PartFunc of X,REAL; ::_thesis: (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)
A1: dom ((R_EAL f) (#) (R_EAL g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) by MESFUNC1:def_5;
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((R_EAL_f)_(#)_(R_EAL_g))_holds_
((R_EAL_f)_(#)_(R_EAL_g))_._x_=_(R_EAL_(f_(#)_g))_._x
let x be Element of X; ::_thesis: ( x in dom ((R_EAL f) (#) (R_EAL g)) implies ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x )
assume A3: x in dom ((R_EAL f) (#) (R_EAL g)) ; ::_thesis: ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x
then  x in dom (f (#) g) by A1, VALUED_1:def_4;
then A4: (f (#) g) . x = (f . x) * (g . x) by VALUED_1:def_4;
 ((R_EAL f) (#) (R_EAL g)) . x = ((R_EAL f) . x) * ((R_EAL g) . x) by A3, MESFUNC1:def_5;
hence  ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x by A4, EXTREAL1:1; ::_thesis: verum
end;
 dom ((R_EAL f) (#) (R_EAL g)) = dom (R_EAL (f (#) g)) by A1, VALUED_1:def_4;
hence  (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) by A2, PARTFUN1:5; ::_thesis: verum
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_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
proof
let X be non empty set ; ::_thesis: 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_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let E be Element of S; ::_thesis: for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let f, g be PartFunc of X,REAL; ::_thesis: ( (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E implies f (#) g is_measurable_on E )
assume that
A1: (dom f) /\ (dom g) = E and
A2: ( f is_measurable_on E & g is_measurable_on E ) ; ::_thesis: f (#) g is_measurable_on E
 ( R_EAL f is_measurable_on E & R_EAL g is_measurable_on E ) by A2, MESFUNC6:def_1;
then  (R_EAL f) (#) (R_EAL g) is_measurable_on E by A1, MESFUNC7:15;
then  R_EAL (f (#) g) is_measurable_on E by Th30;
hence  f (#) g is_measurable_on E by MESFUNC6:def_1; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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)) )
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )
A1: dom ((Re f) (#) (Re g)) = (dom (Re f)) /\ (dom (Re g)) by VALUED_1:def_4;
A2: dom ((Im f) (#) (Im g)) = (dom (Im f)) /\ (dom (Im g)) by VALUED_1:def_4;
A3: dom (Re f) = dom f by COMSEQ_3:def_3;
A4: dom (Im g) = dom g by COMSEQ_3:def_4;
A5: dom (Re g) = dom g by COMSEQ_3:def_3;
A6: dom (Re (f (#) g)) = dom (f (#) g) by COMSEQ_3:def_3;
then A7: dom (Re (f (#) g)) = (dom f) /\ (dom g) by VALUED_1:def_4;
A8: dom (Im f) = dom f by COMSEQ_3:def_4;
A9: dom (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) = (dom ((Re f) (#) (Re g))) /\ (dom ((Im f) (#) (Im g))) by VALUED_1:12;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Re_(f_(#)_g))_holds_
(Re_(f_(#)_g))_._x_=_(((Re_f)_(#)_(Re_g))_-_((Im_f)_(#)_(Im_g)))_._x
let x be set ; ::_thesis: ( x in dom (Re (f (#) g)) implies (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x )
assume A10: x in dom (Re (f (#) g)) ; ::_thesis: (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x
then  (Re (f (#) g)) . x = Re ((f (#) g) . x) by COMSEQ_3:def_3;
then  (Re (f (#) g)) . x = Re ((f . x) * (g . x)) by A6, A10, VALUED_1:def_4;
then A11: (Re (f (#) g)) . x = ((Re (f . x)) * (Re (g . x))) - ((Im (f . x)) * (Im (g . x))) by COMPLEX1:9;
 x in dom g by A7, A10, XBOOLE_0:def_4;
then A12: ( (Re g) . x = Re (g . x) & (Im g) . x = Im (g . x) ) by A5, A4, COMSEQ_3:def_3, COMSEQ_3:def_4;
 x in dom f by A7, A10, XBOOLE_0:def_4;
then  ( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by A3, A8, COMSEQ_3:def_3, COMSEQ_3:def_4;
then  (Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) . x) * ((Im g) . x)) by A7, A1, A3, A5, A10, A11, A12, VALUED_1:def_4;
then  (Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) (#) (Im g)) . x) by A7, A2, A8, A4, A10, VALUED_1:def_4;
hence  (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x by A7, A9, A1, A2, A3, A8, A5, A4, A10, VALUED_1:13; ::_thesis: verum
end;
hence  Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) by A7, A9, A1, A2, A3, A8, A5, A4, FUNCT_1:2; ::_thesis: Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g))
A13: dom ((Im f) (#) (Re g)) = (dom (Im f)) /\ (dom (Re g)) by VALUED_1:def_4;
A14: dom ((Re f) (#) (Im g)) = (dom (Re f)) /\ (dom (Im g)) by VALUED_1:def_4;
A15: dom (Im (f (#) g)) = dom (f (#) g) by COMSEQ_3:def_4;
then A16: dom (Im (f (#) g)) = (dom f) /\ (dom g) by VALUED_1:def_4;
A17: dom (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) = (dom ((Im f) (#) (Re g))) /\ (dom ((Re f) (#) (Im g))) by VALUED_1:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Im_(f_(#)_g))_holds_
(Im_(f_(#)_g))_._x_=_(((Im_f)_(#)_(Re_g))_+_((Re_f)_(#)_(Im_g)))_._x
let x be set ; ::_thesis: ( x in dom (Im (f (#) g)) implies (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x )
assume A18: x in dom (Im (f (#) g)) ; ::_thesis: (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x
then  (Im (f (#) g)) . x = Im ((f (#) g) . x) by COMSEQ_3:def_4;
then  (Im (f (#) g)) . x = Im ((f . x) * (g . x)) by A15, A18, VALUED_1:def_4;
then A19: (Im (f (#) g)) . x = ((Im (f . x)) * (Re (g . x))) + ((Re (f . x)) * (Im (g . x))) by COMPLEX1:9;
 x in dom g by A16, A18, XBOOLE_0:def_4;
then A20: ( (Re g) . x = Re (g . x) & (Im g) . x = Im (g . x) ) by A5, A4, COMSEQ_3:def_3, COMSEQ_3:def_4;
 x in dom f by A16, A18, XBOOLE_0:def_4;
then  ( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by A3, A8, COMSEQ_3:def_3, COMSEQ_3:def_4;
then  (Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) . x) * ((Im g) . x)) by A16, A13, A8, A5, A18, A19, A20, VALUED_1:def_4;
then  (Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) (#) (Im g)) . x) by A16, A14, A3, A4, A18, VALUED_1:def_4;
hence  (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x by A16, A17, A13, A14, A3, A8, A5, A4, A18, VALUED_1:def_1; ::_thesis: verum
end;
hence  Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) by A16, A17, A13, A14, A3, A8, A5, A4, FUNCT_1:2; ::_thesis: verum
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_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
proof
let X be non empty set ; ::_thesis: 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_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,COMPLEX
for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let f, g be PartFunc of X,COMPLEX; ::_thesis: for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let E be Element of S; ::_thesis: ( (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E implies f (#) g is_measurable_on E )
assume that
A1: (dom f) /\ (dom g) = E and
A2: f is_measurable_on E and
A3: g is_measurable_on E ; ::_thesis: f (#) g is_measurable_on E
A4: dom (Im g) = dom g by COMSEQ_3:def_4;
A5: Im f is_measurable_on E by A2, MESFUN6C:def_1;
A6: dom (Im f) = dom f by COMSEQ_3:def_4;
then A7: dom ((Im f) (#) (Im g)) = E by A1, A4, VALUED_1:def_4;
A8: Im g is_measurable_on E by A3, MESFUN6C:def_1;
then A9: (Im f) (#) (Im g) is_measurable_on E by A1, A5, A6, A4, Th31;
A10: dom (Re f) = dom f by COMSEQ_3:def_3;
A11: dom (Re g) = dom g by COMSEQ_3:def_3;
A12: Re g is_measurable_on E by A3, MESFUN6C:def_1;
then A13: (Im f) (#) (Re g) is_measurable_on E by A1, A5, A6, A11, Th31;
A14: Re f is_measurable_on E by A2, MESFUN6C:def_1;
then  (Re f) (#) (Im g) is_measurable_on E by A1, A8, A10, A4, Th31;
then  ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) is_measurable_on E by A13, MESFUNC6:26;
then A15: Im (f (#) g) is_measurable_on E by Th32;
 (Re f) (#) (Re g) is_measurable_on E by A1, A14, A12, A10, A11, Th31;
then  ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) is_measurable_on E by A9, A7, MESFUNC6:29;
then  Re (f (#) g) is_measurable_on E by Th32;
hence  f (#) g is_measurable_on E by A15, MESFUN6C:def_1; ::_thesis: verum
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_measurable_on E & g is_measurable_on E ) & 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
let X be non empty set ; ::_thesis: 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_measurable_on E & g is_measurable_on E ) & 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)
let S be SigmaField of X; ::_thesis: 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_measurable_on E & g is_measurable_on E ) & 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)
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st ex E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & 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)
let f, g be PartFunc of X,REAL; ::_thesis: ( ex E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) implies Integral (M,g) <= Integral (M,f) )
assume that
A1: ex A being Element of S st
( A = dom f & A = dom g & f is_measurable_on A & g is_measurable_on A ) and
A2: ( f is nonnegative & g is nonnegative ) and
A3: for x being Element of X st x in dom g holds
g . x <= f . x ; ::_thesis: Integral (M,g) <= Integral (M,f)
A4: ( Integral (M,g) = integral+ (M,(R_EAL g)) & Integral (M,f) = integral+ (M,(R_EAL f)) ) by A1, A2, MESFUNC6:82;
consider A being Element of S such that
A5: ( A = dom f & A = dom g ) and
A6: ( f is_measurable_on A & g is_measurable_on A ) by A1;
 ( R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by A6, MESFUNC6:def_1;
hence  Integral (M,g) <= Integral (M,f) by A2, A3, A5, A4, MESFUNC5:85; ::_thesis: verum
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_measurable_on A ) & |.f.| is_integrable_on M )
proof
let X be non empty set ; ::_thesis: 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_measurable_on A ) & |.f.| is_integrable_on M )
let S be SigmaField of X; ::_thesis: 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_measurable_on A ) & |.f.| is_integrable_on M )
let M be sigma_Measure of S; ::_thesis: 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_measurable_on A ) & |.f.| is_integrable_on M )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M implies ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M ) )
assume A1: f is_integrable_on M ; ::_thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M )
then  Re f is_integrable_on M by MESFUN6C:def_2;
then  R_EAL (Re f) is_integrable_on M by MESFUNC6:def_4;
then consider A1 being Element of S such that
A2: A1 = dom (R_EAL (Re f)) and
A3: R_EAL (Re f) is_measurable_on A1 by MESFUNC5:def_17;
A4: Re f is_measurable_on A1 by A3, MESFUNC6:def_1;
 Im f is_integrable_on M by A1, MESFUN6C:def_2;
then  R_EAL (Im f) is_integrable_on M by MESFUNC6:def_4;
then consider A2 being Element of S such that
A5: A2 = dom (R_EAL (Im f)) and
A6: R_EAL (Im f) is_measurable_on A2 by MESFUNC5:def_17;
A7: A1 = dom f by A2, COMSEQ_3:def_3;
 A2 = dom f by A5, COMSEQ_3:def_4;
then  Im f is_measurable_on A1 by A6, A7, MESFUNC6:def_1;
then A8: f is_measurable_on A1 by A4, MESFUN6C:def_1;
hence  ex A being Element of S st
( A = dom f & f is_measurable_on A ) by A7; ::_thesis: |.f.| is_integrable_on M
thus  |.f.| is_integrable_on M by A1, A7, A8, MESFUN6C:31; ::_thesis: verum
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 Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (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
let X be non empty set ; ::_thesis: 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 Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (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 ) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (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 ) ) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (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 ) ) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M implies ex F being Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (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 ) ) ) )
assume A1: f is_integrable_on M ; ::_thesis: ex F being Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (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 ) ) )
then consider E being Element of S such that
A2: E = dom f and
A3: f is_measurable_on E by Th35;
defpred S1[ Element of NAT , set ] means $2 = E /\ (great_eq_dom (|.f.|,(1 / ($1 + 1))));
A4: dom |.f.| = E by A2, VALUED_1:def_11;
now__::_thesis:_for_x_being_set_st_x_in_E_\_(eq_dom_(|.f.|,0))_holds_
x_in_E_/\_(great_dom_(|.f.|,0))
let x be set ; ::_thesis: ( x in E \ (eq_dom (|.f.|,0)) implies x in E /\ (great_dom (|.f.|,0)) )
reconsider y = |.f.| . x as Real ;
assume A5: x in E \ (eq_dom (|.f.|,0)) ; ::_thesis: x in E /\ (great_dom (|.f.|,0))
then A6: x in E by XBOOLE_0:def_5;
then A7: x in dom |.f.| by A2, VALUED_1:def_11;
 not x in eq_dom (|.f.|,0) by A5, XBOOLE_0:def_5;
then  not y = 0 by A7, MESFUNC6:7;
then  not |.(f . x).| = 0 by A7, VALUED_1:def_11;
then  f . x <> 0 by COMPLEX1:5, SQUARE_1:17;
then  0 < |.(f . x).| by COMPLEX1:47;
then  0 < |.f.| . x by A7, VALUED_1:def_11;
then  x in great_dom (|.f.|,0) by A7, MESFUNC1:def_13;
hence  x in E /\ (great_dom (|.f.|,0)) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
then A8: E \ (eq_dom (|.f.|,0)) c= E /\ (great_dom (|.f.|,0)) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_E_/\_(great_dom_(|.f.|,0))_holds_
x_in_E_\_(eq_dom_(|.f.|,0))
let x be set ; ::_thesis: ( x in E /\ (great_dom (|.f.|,0)) implies x in E \ (eq_dom (|.f.|,0)) )
assume A9: x in E /\ (great_dom (|.f.|,0)) ; ::_thesis: x in E \ (eq_dom (|.f.|,0))
then  x in great_dom (|.f.|,0) by XBOOLE_0:def_4;
then  0 < |.f.| . x by MESFUNC1:def_13;
then A10: not x in eq_dom (|.f.|,0) by MESFUNC1:def_15;
 x in E by A9, XBOOLE_0:def_4;
hence  x in E \ (eq_dom (|.f.|,0)) by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
then A11: E /\ (great_dom (|.f.|,0)) c= E \ (eq_dom (|.f.|,0)) by TARSKI:def_3;
A12: |.f.| is_measurable_on E by A2, A3, MESFUN6C:30;
A13: for n being Element of NAT ex Z being Element of S st S1[n,Z]
proof
let n be Element of NAT ; ::_thesis: ex Z being Element of S st S1[n,Z]
take  E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ; ::_thesis: ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] )
thus  ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] ) by A12, A4, MESFUNC6:13; ::_thesis: verum
end;
consider F being Function of NAT,S such that
A14: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A13);
A15: for n being Nat holds
( F . n in S & M . (F . n) < +infty )
proof
 |.f.| is_integrable_on M by A1, Th35;
then A16: Integral (M,|.f.|) < +infty by MESFUNC6:90;
let n be Nat; ::_thesis: ( F . n in S & M . (F . n) < +infty )
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
set z = R_EAL (1 / (n + 1));
A17: F . n1 = E /\ (great_eq_dom (|.f.|,(1 / (n1 + 1)))) by A14;
then reconsider En = F . n as Element of S ;
set h = |.f.| | En;
consider nf being PartFunc of X,REAL such that
A18: nf is_simple_func_in S and
A19: dom nf = En and
A20: for x being set st x in En holds
nf . x = 1 / (n + 1) by MESFUNC6:75;
A21: dom (|.f.| | En) = En by A4, A17, RELAT_1:62, XBOOLE_1:17;
A22: F . n c= great_eq_dom (|.f.|,(1 / (n + 1))) by A17, XBOOLE_1:17;
A23: for x being Element of X st x in dom nf holds
nf . x <= (|.f.| | En) . x
proof
let x be Element of X; ::_thesis: ( x in dom nf implies nf . x <= (|.f.| | En) . x )
assume A24: x in dom nf ; ::_thesis: nf . x <= (|.f.| | En) . x
then  (|.f.| | En) . x = |.f.| . x by A19, FUNCT_1:49;
then  1 / (n + 1) <= (|.f.| | En) . x by A22, A19, A24, MESFUNC1:def_14;
hence  nf . x <= (|.f.| | En) . x by A19, A20, A24; ::_thesis: verum
end;
 (dom |.f.|) /\ En = E /\ En by A2, VALUED_1:def_11;
then A25: (dom |.f.|) /\ En = En by A17, XBOOLE_1:17, XBOOLE_1:28;
 |.f.| is_measurable_on En by A12, A17, MESFUNC6:16, XBOOLE_1:17;
then A26: |.f.| | En is_measurable_on En by A25, MESFUNC6:76;
A27: |.f.| | En is nonnegative by Lm1, MESFUNC6:55;
 for x being set st x in dom nf holds
nf . x >= 0 by A19, A20;
then A28: nf is nonnegative by MESFUNC6:52;
 ( |.f.| is nonnegative & |.f.| | E = |.f.| ) by A4, Lm1, RELAT_1:69;
then A29: Integral (M,(|.f.| | En)) <= Integral (M,|.f.|) by A12, A4, A17, MESFUNC6:87, XBOOLE_1:17;
 nf is_measurable_on En by A18, MESFUNC6:50;
then  Integral (M,nf) <= Integral (M,(|.f.| | En)) by A21, A26, A27, A19, A28, A23, Th34;
then A30: Integral (M,nf) <= Integral (M,|.f.|) by A29, XXREAL_0:2;
A31: ( ((R_EAL (1 / (n + 1))) * (M . En)) / (R_EAL (1 / (n + 1))) = M . En & +infty / (R_EAL (1 / (n + 1))) = +infty ) by XXREAL_3:83, XXREAL_3:88;
 Integral (M,nf) = (R_EAL (1 / (n + 1))) * (M . En) by A19, A20, MESFUNC6:97;
then  (R_EAL (1 / (n + 1))) * (M . En) < +infty by A16, A30, XXREAL_0:2;
hence  ( F . n in S & M . (F . n) < +infty ) by A31, XXREAL_3:80; ::_thesis: verum
end;
take  F ; ::_thesis: ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (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 ) ) )
A32: for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))
proof
let n be Nat; ::_thesis: F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))
 n in NAT by ORDINAL1:def_12;
hence  F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) by A14; ::_thesis: verum
end;
then  for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(0 + (1 / (n + 1))))) ;
then  E /\ (great_dom (|.f.|,0)) = union (rng F) by MESFUNC6:11;
hence  ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (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 ) ) ) by A2, A32, A11, A8, A15, XBOOLE_0:def_10; ::_thesis: verum
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
let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX
for A being set holds |.f.| | A = |.(f | A).|
let f be PartFunc of X,COMPLEX; ::_thesis: for A being set holds |.f.| | A = |.(f | A).|
let A be set ; ::_thesis: |.f.| | A = |.(f | A).|
 dom (|.f.| | A) = (dom |.f.|) /\ A by RELAT_1:61;
then A1: dom (|.f.| | A) = (dom f) /\ A by VALUED_1:def_11;
A2: dom (f | A) = (dom f) /\ A by RELAT_1:61;
then A3: dom |.(f | A).| = (dom f) /\ A by VALUED_1:def_11;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(|.f.|_|_A)_holds_
(|.f.|_|_A)_._x_=_|.(f_|_A).|_._x
let x be Element of X; ::_thesis: ( x in dom (|.f.| | A) implies (|.f.| | A) . x = |.(f | A).| . x )
assume A4: x in dom (|.f.| | A) ; ::_thesis: (|.f.| | A) . x = |.(f | A).| . x
then  |.(f | A).| . x = |.((f | A) . x).| by A1, A3, VALUED_1:def_11;
then A5: |.(f | A).| . x = |.(f . x).| by A2, A1, A4, FUNCT_1:47;
 x in dom f by A1, A4, XBOOLE_0:def_4;
then A6: x in dom |.f.| by VALUED_1:def_11;
 (|.f.| | A) . x = |.f.| . x by A4, FUNCT_1:47;
hence  (|.f.| | A) . x = |.(f | A).| . x by A6, A5, VALUED_1:def_11; ::_thesis: verum
end;
hence  |.f.| | A = |.(f | A).| by A1, A3, PARTFUN1:5; ::_thesis: verum
end;

theorem Th38: :: MESFUN7C:38
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds
( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX holds
( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
 dom (|.f.| + |.g.|) = (dom |.f.|) /\ (dom |.g.|) by VALUED_1:def_1;
then  dom (|.f.| + |.g.|) = (dom f) /\ (dom |.g.|) by VALUED_1:def_11;
hence  dom (|.f.| + |.g.|) = (dom f) /\ (dom g) by VALUED_1:def_11; ::_thesis: dom |.(f + g).| c= dom |.f.|
dom |.(f + g).| = dom (f + g) by VALUED_1:def_11
.= (dom f) /\ (dom g) by VALUED_1:def_1 ;
then  dom |.(f + g).| c= dom f by XBOOLE_1:17;
hence  dom |.(f + g).| c= dom |.f.| by VALUED_1:def_11; ::_thesis: verum
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).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
let f, g be PartFunc of X,COMPLEX; ::_thesis: (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
A1: dom |.(f + g).| c= dom |.g.| by Th38;
then A2: dom |.(f + g).| c= dom g by VALUED_1:def_11;
 dom (g | (dom |.(f + g).|)) = (dom g) /\ (dom |.(f + g).|) by RELAT_1:61;
then A3: dom (g | (dom |.(f + g).|)) = dom |.(f + g).| by A2, XBOOLE_1:28;
then A4: dom |.(g | (dom |.(f + g).|)).| = dom |.(f + g).| by VALUED_1:def_11;
A5: dom |.(f + g).| c= dom |.f.| by Th38;
then A6: dom |.(f + g).| c= dom f by VALUED_1:def_11;
then  (dom |.(f + g).|) /\ (dom |.(f + g).|) c= (dom f) /\ (dom g) by A2, XBOOLE_1:27;
then A7: dom |.(f + g).| c= dom (|.f.| + |.g.|) by Th38;
then A8: dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) = dom |.(f + g).| by RELAT_1:62;
 dom (f | (dom |.(f + g).|)) = (dom f) /\ (dom |.(f + g).|) by RELAT_1:61;
then A9: dom (f | (dom |.(f + g).|)) = dom |.(f + g).| by A6, XBOOLE_1:28;
A10: ( |.f.| | (dom |.(f + g).|) = |.(f | (dom |.(f + g).|)).| & |.g.| | (dom |.(f + g).|) = |.(g | (dom |.(f + g).|)).| ) by Th37;
then A11: dom ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) = (dom (f | (dom |.(f + g).|))) /\ (dom (g | (dom |.(f + g).|))) by Th38
.= dom |.(f + g).| by A9, A3 ;
A12: dom |.(f | (dom |.(f + g).|)).| = dom |.(f + g).| by A9, VALUED_1:def_11;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((|.f.|_+_|.g.|)_|_(dom_|.(f_+_g).|))_holds_
((|.f.|_+_|.g.|)_|_(dom_|.(f_+_g).|))_._x_=_((|.f.|_|_(dom_|.(f_+_g).|))_+_(|.g.|_|_(dom_|.(f_+_g).|)))_._x
let x be Element of X; ::_thesis: ( x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) implies ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x )
assume A13: x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) ; ::_thesis: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x
then A14: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = (|.f.| + |.g.|) . x by FUNCT_1:47
.= (|.f.| . x) + (|.g.| . x) by A7, A8, A13, VALUED_1:def_1
.= |.(f . x).| + (|.g.| . x) by A5, A8, A13, VALUED_1:def_11 ;
A15: x in dom |.(f + g).| by A7, A13, RELAT_1:62;
then ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x = ((|.f.| | (dom |.(f + g).|)) . x) + ((|.g.| | (dom |.(f + g).|)) . x) by A11, VALUED_1:def_1
.= |.((f | (dom |.(f + g).|)) . x).| + (|.(g | (dom |.(f + g).|)).| . x) by A12, A10, A15, VALUED_1:def_11
.= |.((f | (dom |.(f + g).|)) . x).| + |.((g | (dom |.(f + g).|)) . x).| by A4, A15, VALUED_1:def_11
.= |.(f . x).| + |.((g | (dom |.(f + g).|)) . x).| by A15, FUNCT_1:49
.= |.(f . x).| + |.(g . x).| by A15, FUNCT_1:49 ;
hence  ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x by A1, A8, A13, A14, VALUED_1:def_11; ::_thesis: verum
end;
hence  (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) by A11, A7, PARTFUN1:5, RELAT_1:62; ::_thesis: verum
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 <= (|.f.| + |.g.|) . x
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let f, g be PartFunc of X,COMPLEX; ::_thesis: for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let x be set ; ::_thesis: ( x in dom |.(f + g).| implies |.(f + g).| . x <= (|.f.| + |.g.|) . x )
A1: |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by COMPLEX1:56;
assume A2: x in dom |.(f + g).| ; ::_thesis: |.(f + g).| . x <= (|.f.| + |.g.|) . x
then  x in dom (f + g) by VALUED_1:def_11;
then A3: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by A1, VALUED_1:def_1;
A4: dom |.(f + g).| c= dom |.g.| by Th38;
then A5: |.(g . x).| = |.g.| . x by A2, VALUED_1:def_11;
 x in dom |.g.| by A2, A4;
then A6: x in dom g by VALUED_1:def_11;
A7: dom |.(f + g).| c= dom |.f.| by Th38;
then  x in dom |.f.| by A2;
then  x in dom f by VALUED_1:def_11;
then  x in (dom f) /\ (dom g) by A6, XBOOLE_0:def_4;
then A8: x in dom (|.f.| + |.g.|) by Th38;
 |.(f . x).| = |.f.| . x by A2, A7, VALUED_1:def_11;
then  |.(f . x).| + |.(g . x).| = (|.f.| + |.g.|) . x by A5, A8, VALUED_1:def_1;
hence  |.(f + g).| . x <= (|.f.| + |.g.|) . x by A2, A3, VALUED_1:def_11; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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
let f, g be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in dom f holds
f . x <= g . x ) implies g - f is nonnegative )
assume A1: for x being set st x in dom f holds
f . x <= g . x ; ::_thesis: g - f is nonnegative
now__::_thesis:_for_x_being_set_st_x_in_dom_(g_-_f)_holds_
0_<=_(g_-_f)_._x
let x be set ; ::_thesis: ( x in dom (g - f) implies 0 <= (g - f) . x )
assume A2: x in dom (g - f) ; ::_thesis: 0 <= (g - f) . x
then  x in (dom g) /\ (dom f) by VALUED_1:12;
then  x in dom f by XBOOLE_0:def_4;
then  0 <= (g . x) - (f . x) by A1, XREAL_1:48;
hence  0 <= (g - f) . x by A2, VALUED_1:13; ::_thesis: verum
end;
hence  g - f is nonnegative by MESFUNC6:52; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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))) )
let S be SigmaField of X; ::_thesis: 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))) )
let M be sigma_Measure of S; ::_thesis: 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))) )
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
 ( |.f.| is_integrable_on M & |.g.| is_integrable_on M ) by A1, A2, Th35;
then A3: |.f.| + |.g.| is_integrable_on M by MESFUNC6:100;
 Im g is_integrable_on M by A2, MESFUN6C:def_2;
then  R_EAL (Im g) is_integrable_on M by MESFUNC6:def_4;
then consider B2 being Element of S such that
A4: ( B2 = dom (R_EAL (Im g)) & R_EAL (Im g) is_measurable_on B2 ) by MESFUNC5:def_17;
 Im f is_integrable_on M by A1, MESFUN6C:def_2;
then  R_EAL (Im f) is_integrable_on M by MESFUNC6:def_4;
then consider A2 being Element of S such that
A5: ( A2 = dom (R_EAL (Im f)) & R_EAL (Im f) is_measurable_on A2 ) by MESFUNC5:def_17;
 Re g is_integrable_on M by A2, MESFUN6C:def_2;
then  R_EAL (Re g) is_integrable_on M by MESFUNC6:def_4;
then consider B1 being Element of S such that
A6: B1 = dom (R_EAL (Re g)) and
A7: R_EAL (Re g) is_measurable_on B1 by MESFUNC5:def_17;
A8: B1 = dom g by A6, COMSEQ_3:def_3;
 f + g is_integrable_on M by A1, A2, MESFUN6C:33;
then A9: |.(f + g).| is_integrable_on M by Th35;
set G = |.g.|;
set F = |.f.|;
 for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x by Th40;
then A10: (|.f.| + |.g.|) - |.(f + g).| is nonnegative by Th41;
 Re f is_integrable_on M by A1, MESFUN6C:def_2;
then  R_EAL (Re f) is_integrable_on M by MESFUNC6:def_4;
then consider A1 being Element of S such that
A11: A1 = dom (R_EAL (Re f)) and
A12: R_EAL (Re f) is_measurable_on A1 by MESFUNC5:def_17;
A13: A1 = dom f by A11, COMSEQ_3:def_3;
reconsider A = A1 /\ B1 as Element of S ;
 Re f is_measurable_on A1 by A12, MESFUNC6:def_1;
then A14: Re f is_measurable_on A by MESFUNC6:16, XBOOLE_1:17;
A15: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
then A16: dom |.(f + g).| = A by A13, A8, VALUED_1:def_11;
 Re g is_measurable_on B1 by A7, MESFUNC6:def_1;
then A17: Re g is_measurable_on A by MESFUNC6:16, XBOOLE_1:17;
 ( B2 = dom g & Im g is_measurable_on B2 ) by A4, COMSEQ_3:def_4, MESFUNC6:def_1;
then  Im g is_measurable_on A by A8, MESFUNC6:16, XBOOLE_1:17;
then A18: g is_measurable_on A by A17, MESFUN6C:def_1;
then A19: |.g.| is_measurable_on A by A8, MESFUN6C:30, XBOOLE_1:17;
 ( A2 = dom f & Im f is_measurable_on A2 ) by A5, COMSEQ_3:def_4, MESFUNC6:def_1;
then  Im f is_measurable_on A by A13, MESFUNC6:16, XBOOLE_1:17;
then A20: f is_measurable_on A by A14, MESFUN6C:def_1;
then  |.f.| is_measurable_on A by A13, MESFUN6C:30, XBOOLE_1:17;
then A21: |.f.| + |.g.| is_measurable_on A by A19, MESFUNC6:26;
 A c= A1 by XBOOLE_1:17;
then A22: A c= dom |.f.| by A13, VALUED_1:def_11;
 A c= B1 by XBOOLE_1:17;
then A23: A c= dom |.g.| by A8, VALUED_1:def_11;
A24: dom (|.f.| + |.g.|) = (dom |.f.|) /\ (dom |.g.|) by VALUED_1:def_1;
then A25: (dom |.(f + g).|) /\ (dom (|.f.| + |.g.|)) = A by A22, A23, A16, XBOOLE_1:19, XBOOLE_1:28;
 |.(f + g).| is_measurable_on A by A13, A8, A20, A18, A15, MESFUN6C:11, MESFUN6C:30;
then consider E being Element of S such that
A26: E = (dom (|.f.| + |.g.|)) /\ (dom |.(f + g).|) and
A27: Integral (M,(|.(f + g).| | E)) <= Integral (M,((|.f.| + |.g.|) | E)) by A21, A3, A25, A9, A10, MESFUN6C:42;
A28: dom (|.g.| | E) = E by A23, A25, A26, RELAT_1:62;
take  E ; ::_thesis: ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
thus  E = dom (f + g) by A13, A8, A15, A24, A22, A23, A16, A26, XBOOLE_1:19, XBOOLE_1:28; ::_thesis: Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E)))
 ( |.f.| | E is_integrable_on M & |.g.| | E is_integrable_on M ) by A1, A2, Th35, MESFUNC6:91;
then consider E1 being Element of S such that
A29: E1 = (dom (|.f.| | E)) /\ (dom (|.g.| | E)) and
A30: Integral (M,((|.f.| | E) + (|.g.| | E))) = (Integral (M,((|.f.| | E) | E1))) + (Integral (M,((|.g.| | E) | E1))) by MESFUNC6:101;
 dom (|.f.| | E) = E by A22, A25, A26, RELAT_1:62;
then  ( (|.f.| | E) | E1 = |.f.| | E & (|.g.| | E) | E1 = |.g.| | E ) by A29, A28, FUNCT_1:51;
hence  Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) by A16, A25, A26, A27, A30, Th39; ::_thesis: verum
end;

begin

definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,COMPLEX;
predf is_simple_func_in S means :Def13: :: 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 Def13 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 ;
predF,a are_Re-presentation_of f means :Def14: :: 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 Def14 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 ;
predF,a are_Re-presentation_of f means :Def15: :: 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 Def15 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
let X be non empty set ; ::_thesis: 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 ) )
let S be SigmaField of X; ::_thesis: 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 ) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )
hereby  ::_thesis: ( Re f is_simple_func_in S & Im f is_simple_func_in S implies f is_simple_func_in S )
assume  f is_simple_func_in S ; ::_thesis: ( Re f is_simple_func_in S & Im f is_simple_func_in S )
then consider F being Finite_Sep_Sequence of S such that
A1: dom f = union (rng F) and
A2: 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 by Def13;
A3: dom (Im f) = union (rng F) by A1, COMSEQ_3:def_4;
A4: 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
(Im f) . x = (Im f) . y
proof
let n be Nat; ::_thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(Im f) . x = (Im f) . y
let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies (Im f) . x = (Im f) . y )
assume that
A5: n in dom F and
A6: ( x in F . n & y in F . n ) ; ::_thesis: (Im f) . x = (Im f) . y
 F . n c= union (rng F) by A5, MESFUNC3:7;
then  ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by A3, A6, COMSEQ_3:def_4;
hence  (Im f) . x = (Im f) . y by A2, A5, A6; ::_thesis: verum
end;
A7: dom (Re f) = union (rng F) by A1, COMSEQ_3:def_3;
 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
(Re f) . x = (Re f) . y
proof
let n be Nat; ::_thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(Re f) . x = (Re f) . y
let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies (Re f) . x = (Re f) . y )
assume that
A8: n in dom F and
A9: ( x in F . n & y in F . n ) ; ::_thesis: (Re f) . x = (Re f) . y
 F . n c= union (rng F) by A8, MESFUNC3:7;
then  ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by A7, A9, COMSEQ_3:def_3;
hence  (Re f) . x = (Re f) . y by A2, A8, A9; ::_thesis: verum
end;
hence  ( Re f is_simple_func_in S & Im f is_simple_func_in S ) by A7, A3, A4, MESFUNC6:def_2; ::_thesis: verum
end;
assume that
A10: Re f is_simple_func_in S and
A11: Im f is_simple_func_in S ; ::_thesis: f is_simple_func_in S
consider F being Finite_Sep_Sequence of S such that
A12: dom (Re f) = union (rng F) and
A13: 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
(Re f) . x = (Re f) . y by A10, MESFUNC6:def_2;
set la = len F;
A14: dom f = union (rng F) by A12, COMSEQ_3:def_3;
consider G being Finite_Sep_Sequence of S such that
A15: dom (Im f) = union (rng G) and
A16: for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(Im f) . x = (Im f) . y by A11, MESFUNC6:def_2;
set lb = len G;
deffunc H1( Nat) ->  set = (F . ((($1 -' 1) div (len G)) + 1)) /\ (G . ((($1 -' 1) mod (len G)) + 1));
consider FG being FinSequence such that
A17: len FG = (len F) * (len G) and
A18: for k being Nat st k in dom FG holds
FG . k = H1(k) from FINSEQ_1:sch_2();
A19: dom FG = Seg ((len F) * (len G)) by A17, FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_FG_holds_
FG_._k_in_S
let k be Nat; ::_thesis: ( k in dom FG implies FG . k in S )
A20: len G divides (len F) * (len G) by NAT_D:def_3;
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
assume A21: k in dom FG ; ::_thesis: FG . k in S
then A22: 1 <= k by FINSEQ_3:25;
then A23: len G > 0 by A17, A21, FINSEQ_3:25;
A24: k <= (len F) * (len G) by A17, A21, FINSEQ_3:25;
then  k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
then A25: (k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G) by NAT_2:24;
A26: 1 <= (len F) * (len G) by A22, A24, XXREAL_0:2;
 1 <= len G by A23, NAT_1:14;
then  (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A26, A20, NAT_2:15;
then  ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by A25, XREAL_1:19;
then  ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A23, NAT_1:14, NAT_D:18;
then  ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_3:25;
then A27: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:3;
 (k -' 1) mod (len G) < len G by A23, NAT_D:1;
then  ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;
then  ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
then  G . (((k -' 1) mod (len G)) + 1) in rng G by FUNCT_1:3;
then  (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S by A27, MEASURE1:34;
hence  FG . k in S by A18, A21; ::_thesis: verum
end;
then reconsider FG = FG as FinSequence of S by FINSEQ_2:12;
 for k, l being Nat st k in dom FG & l in dom FG & k <> l holds
FG . k misses FG . l
proof
let k, l be Nat; ::_thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )
assume that
A28: k in dom FG and
A29: l in dom FG and
A30: k <> l ; ::_thesis: FG . k misses FG . l
set m = ((l -' 1) mod (len G)) + 1;
set n = ((l -' 1) div (len G)) + 1;
A31: 1 <= k by A28, FINSEQ_3:25;
then A32: len G > 0 by A17, A28, FINSEQ_3:25;
then A33: (l -' 1) + 1 = ((((((l -' 1) div (len G)) + 1) - 1) * (len G)) + ((((l -' 1) mod (len G)) + 1) - 1)) + 1 by NAT_D:2;
A34: k <= (len F) * (len G) by A17, A28, FINSEQ_3:25;
then A35: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A31, NAT_1:14, NAT_D:def_3;
 1 <= len G by A32, NAT_1:14;
then A36: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A35, NAT_2:15;
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
 FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A28;
then A37: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A18, A29
.= (F . (((k -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16
.= (F . (((k -' 1) div (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16
.= ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by XBOOLE_1:16 ;
 l <= (len F) * (len G) by A17, A29, FINSEQ_3:25;
then  l -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
then  (l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A36, NAT_2:24;
then  ((l -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then  ( ((l -' 1) div (len G)) + 1 >= 1 & ((l -' 1) div (len G)) + 1 <= len F ) by A32, NAT_1:14, NAT_D:18;
then  ((l -' 1) div (len G)) + 1 in Seg (len F) ;
then A38: ((l -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3;
 1 <= l by A29, FINSEQ_3:25;
then A39: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by A33, XREAL_1:233;
 (l -' 1) mod (len G) < len G by A32, NAT_D:1;
then  ( ((l -' 1) mod (len G)) + 1 >= 1 & ((l -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;
then  ((l -' 1) mod (len G)) + 1 in Seg (len G) ;
then A40: ((l -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def_3;
 k -' 1 <= ((len F) * (len G)) -' 1 by A34, NAT_D:42;
then  (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A36, NAT_2:24;
then  ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then  ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A32, NAT_1:11, NAT_D:18;
then  ((k -' 1) div (len G)) + 1 in Seg (len F) ;
then A41: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3;
 (k -' 1) + 1 = ((((((k -' 1) div (len G)) + 1) - 1) * (len G)) + ((((k -' 1) mod (len G)) + 1) - 1)) + 1 by A32, NAT_D:2;
then A42: (k - 1) + 1 = (((((k -' 1) div (len G)) + 1) - 1) * (len G)) + (((k -' 1) mod (len G)) + 1) by A31, XREAL_1:233;
 (k -' 1) mod (len G) < len G by A32, NAT_D:1;
then  ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:11, NAT_1:13;
then  ((k -' 1) mod (len G)) + 1 in Seg (len G) ;
then A43: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def_3;
percases ( ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 or ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ) by A30, A42, A39;
suppose ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 ; ::_thesis: FG . k misses FG . l
then  F . (((k -' 1) div (len G)) + 1) misses F . (((l -' 1) div (len G)) + 1) by A41, A38, MESFUNC3:4;
then  (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A37, XBOOLE_0:def_7;
hence  FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum
end;
suppose ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ; ::_thesis: FG . k misses FG . l
then  G . (((k -' 1) mod (len G)) + 1) misses G . (((l -' 1) mod (len G)) + 1) by A43, A40, MESFUNC3:4;
then  (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ {} by A37, XBOOLE_0:def_7;
hence  FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A44: dom f = union (rng G) by A15, COMSEQ_3:def_4;
A45: dom f = union (rng FG)
proof
thus  dom f c= union (rng FG) :: according to XBOOLE_0:def_10 ::_thesis: union (rng FG) c= dom f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom f or z in union (rng FG) )
assume A46: z in dom f ; ::_thesis: z in union (rng FG)
then consider Y being set  such that
A47: z in Y and
A48: Y in rng F by A14, TARSKI:def_4;
consider Z being set  such that
A49: z in Z and
A50: Z in rng G by A44, A46, TARSKI:def_4;
consider j being Nat such that
A51: j in dom G and
A52: Z = G . j by A50, FINSEQ_2:10;
consider i being Nat such that
A53: i in dom F and
A54: F . i = Y by A48, FINSEQ_2:10;
 1 <= i by A53, FINSEQ_3:25;
then consider i9 being Nat such that
A55: i = 1 + i9 by NAT_1:10;
set k = ((i - 1) * (len G)) + j;
reconsider k = ((i - 1) * (len G)) + j as Nat by A55;
 i <= len F by A53, FINSEQ_3:25;
then  i - 1 <= (len F) - 1 by XREAL_1:9;
then  (i - 1) * (len G) <= ((len F) - 1) * (len G) by XREAL_1:64;
then A56: k <= (((len F) - 1) * (len G)) + j by XREAL_1:6;
A57: j <= len G by A51, FINSEQ_3:25;
then  (((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G) by XREAL_1:6;
then A58: k <= (len F) * (len G) by A56, XXREAL_0:2;
A59: 1 <= j by A51, FINSEQ_3:25;
then consider j9 being Nat such that
A60: j = 1 + j9 by NAT_1:10;
A61: j9 < len G by A57, A60, NAT_1:13;
A62: k >= j by A55, NAT_1:11;
then A63: k -' 1 = k - 1 by A59, XREAL_1:233, XXREAL_0:2
.= (i9 * (len G)) + j9 by A55, A60 ;
then A64: i = ((k -' 1) div (len G)) + 1 by A55, A61, NAT_D:def_1;
A65: k >= 1 by A59, A62, XXREAL_0:2;
then A66: k in Seg ((len F) * (len G)) by A58, FINSEQ_1:1;
A67: j = ((k -' 1) mod (len G)) + 1 by A60, A63, A61, NAT_D:def_2;
 k in dom FG by A17, A65, A58, FINSEQ_3:25;
then A68: FG . k in rng FG by FUNCT_1:def_3;
 z in (F . i) /\ (G . j) by A47, A54, A49, A52, XBOOLE_0:def_4;
then  z in FG . k by A18, A19, A64, A67, A66;
hence  z in union (rng FG) by A68, TARSKI:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union (rng FG) or z in dom f )
assume  z in union (rng FG) ; ::_thesis: z in dom f
then consider Y being set  such that
A69: z in Y and
A70: Y in rng FG by TARSKI:def_4;
consider k being Nat such that
A71: k in dom FG and
A72: FG . k = Y by A70, FINSEQ_2:10;
A73: 1 <= k by A71, FINSEQ_3:25;
then A74: len G > 0 by A17, A71, FINSEQ_3:25;
then A75: 1 <= len G by NAT_1:14;
A76: k <= (len F) * (len G) by A17, A71, FINSEQ_3:25;
then  ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A73, NAT_1:14, NAT_D:def_3;
then A77: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A75, NAT_2:15;
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
 k -' 1 <= ((len F) * (len G)) -' 1 by A76, NAT_D:42;
then  (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A77, NAT_2:24;
then A78: ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) ) by NAT_1:14, XREAL_1:19;
 ((len F) * (len G)) div (len G) = len F by A74, NAT_D:18;
then  ((k -' 1) div (len G)) + 1 in dom F by A78, FINSEQ_3:25;
then A79: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:def_3;
 FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A71;
then  z in F . (((k -' 1) div (len G)) + 1) by A69, A72, XBOOLE_0:def_4;
hence  z in dom f by A14, A79, TARSKI:def_4; ::_thesis: verum
end;
 for k being Nat
for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
f . x = f . y
proof
let k be Nat; ::_thesis: for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
f . x = f . y
let x, y be Element of X; ::_thesis: ( k in dom FG & x in FG . k & y in FG . k implies f . x = f . y )
set i = ((k -' 1) div (len G)) + 1;
set j = ((k -' 1) mod (len G)) + 1;
assume that
A80: k in dom FG and
A81: ( x in FG . k & y in FG . k ) ; ::_thesis: f . x = f . y
A82: FG . k c= union (rng FG) by A80, MESFUNC3:7;
then  FG . k c= dom (Im f) by A45, COMSEQ_3:def_4;
then A83: ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by A81, COMSEQ_3:def_4;
A84: 1 <= k by A80, FINSEQ_3:25;
then A85: len G > 0 by A17, A80, FINSEQ_3:25;
then  (k -' 1) mod (len G) < len G by NAT_D:1;
then  ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;
then A86: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
 FG . k c= dom (Re f) by A45, A82, COMSEQ_3:def_3;
then A87: ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by A81, COMSEQ_3:def_3;
A88: k <= (len F) * (len G) by A17, A80, FINSEQ_3:25;
then A89: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
A90: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A80;
then  ( x in G . (((k -' 1) mod (len G)) + 1) & y in G . (((k -' 1) mod (len G)) + 1) ) by A81, XBOOLE_0:def_4;
then A91: Im (f . x) = Im (f . y) by A16, A86, A83;
A92: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A84, A88, NAT_1:14, NAT_D:def_3;
 1 <= len G by A85, NAT_1:14;
then  (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A92, NAT_2:15;
then  (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A89, NAT_2:24;
then  ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then  ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A85, NAT_1:14, NAT_D:18;
then A93: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_3:25;
 ( x in F . (((k -' 1) div (len G)) + 1) & y in F . (((k -' 1) div (len G)) + 1) ) by A81, A90, XBOOLE_0:def_4;
then  Re (f . x) = Re (f . y) by A13, A93, A87;
hence  f . x = f . y by A91, COMPLEX1:def_3; ::_thesis: verum
end;
hence  f is_simple_func_in S by A45, Def13; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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 ) )
let S be SigmaField of X; ::_thesis: 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 ) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S implies 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 ) ) )
assume  f is_simple_func_in S ; ::_thesis: 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 ) )
then consider F being Finite_Sep_Sequence of S such that
A1: dom f = union (rng F) and
A2: 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 by Def13;
defpred S1[ set , set ] means  for x being set st x in F . $1 holds
$2 = f . x;
A3: for k being Nat st k in Seg (len F) holds
ex y being Element of COMPLEX st S1[k,y]
proof
let k be Nat; ::_thesis: ( k in Seg (len F) implies ex y being Element of COMPLEX st S1[k,y] )
assume  k in Seg (len F) ; ::_thesis: ex y being Element of COMPLEX st S1[k,y]
then A4: k in dom F by FINSEQ_1:def_3;
then A5: F . k in rng F by FUNCT_1:3;
percases ( F . k = {} or F . k <> {} ) ;
supposeA6: F . k = {} ; ::_thesis: ex y being Element of COMPLEX st S1[k,y]
reconsider y = 0 as Element of COMPLEX by NUMBERS:11, TARSKI:def_3;
take  y ; ::_thesis: S1[k,y]
thus  S1[k,y] by A6; ::_thesis: verum
end;
suppose F . k <> {} ; ::_thesis: ex y being Element of COMPLEX st S1[k,y]
then consider x1 being set  such that
A7: x1 in F . k by XBOOLE_0:def_1;
 x1 in dom f by A1, A5, A7, TARSKI:def_4;
then  f . x1 in rng f by FUNCT_1:3;
then reconsider y = f . x1 as Element of COMPLEX ;
take  y ; ::_thesis: S1[k,y]
hereby  ::_thesis: verum
let x be set ; ::_thesis: ( x in F . k implies y = f . x )
A8: rng F c= bool X by XBOOLE_1:1;
assume  x in F . k ; ::_thesis: y = f . x
hence  y = f . x by A2, A4, A5, A7, A8; ::_thesis: verum
end;
end;
end;
end;
consider a being FinSequence of COMPLEX  such that
A9: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S1[k,a . k] ) ) from FINSEQ_1:sch_5(A3);
take  F ; ::_thesis: 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 ) )
take  a ; ::_thesis: ( 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 ) )
now__::_thesis:_for_n_being_Nat_st_n_in_dom_F_holds_
for_x_being_set_st_x_in_F_._n_holds_
a_._n_=_f_._x
let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds
a . n = f . x )
assume  n in dom F ; ::_thesis: for x being set st x in F . n holds
a . n = f . x
then  n in Seg (len F) by FINSEQ_1:def_3;
hence  for x being set st x in F . n holds
a . n = f . x by A9; ::_thesis: verum
end;
hence  ( 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 ) ) by A1, A9, FINSEQ_1:def_3; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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 )
let S be SigmaField of X; ::_thesis: 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 )
let f be PartFunc of X,COMPLEX; ::_thesis: ( 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 )
hereby  ::_thesis: ( ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f implies f is_simple_func_in S )
assume  f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f
then consider F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX  such that
A1: ( 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 ) ) by Th44;
take F = F; ::_thesis: ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f
take a = a; ::_thesis: F,a are_Re-presentation_of f
thus  F,a are_Re-presentation_of f by A1, Def15; ::_thesis: verum
end;
given F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX  such that A2: F,a are_Re-presentation_of f ; ::_thesis: f is_simple_func_in S
A3: 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
proof
let n be Nat; ::_thesis: 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
let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y )
assume that
A4: n in dom F and
A5: x in F . n and
A6: y in F . n ; ::_thesis: f . x = f . y
 f . x = a . n by A2, A4, A5, Def15;
hence  f . x = f . y by A2, A4, A6, Def15; ::_thesis: verum
end;
 dom f = union (rng F) by A2, Def15;
hence  f is_simple_func_in S by A3, Def13; ::_thesis: verum
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
let c be FinSequence of COMPLEX ; ::_thesis: for n being Nat st n in dom (Re c) holds
(Re c) . n = Re (c . n)
let n be Nat; ::_thesis: ( n in dom (Re c) implies (Re c) . n = Re (c . n) )
A1: ((1 / 2) * (c *')) . n = (1 / 2) * ((c *') . n) by COMPLSP2:16;
 ( len ((1 / 2) * c) = len c & len ((1 / 2) * (c *')) = len (c *') ) by COMPLSP2:3;
then A2: len ((1 / 2) * c) = len ((1 / 2) * (c *')) by COMPLSP2:def_1;
 len (c *') = len c by COMPLSP2:def_1;
then  ( n in NAT & (1 / 2) * (c + (c *')) = ((1 / 2) * c) + ((1 / 2) * (c *')) ) by COMPLSP2:30, ORDINAL1:def_12;
then A3: (Re c) . n = (((1 / 2) * c) . n) + (((1 / 2) * (c *')) . n) by A2, COMPLSP2:26;
assume A4: n in dom (Re c) ; ::_thesis: (Re c) . n = Re (c . n)
then  n <= len (Re c) by FINSEQ_3:25;
then A5: n <= len c by COMPLSP2:48;
 1 <= n by A4, FINSEQ_3:25;
then  ((1 / 2) * (c *')) . n = (1 / 2) * ((c . n) *') by A5, A1, COMPLSP2:def_1;
then A6: (Re c) . n = ((1 / 2) * (c . n)) + ((1 / 2) * ((c . n) *')) by A3, COMPLSP2:16;
 c . n = (Re (c . n)) + ((Im (c . n)) * <i>) by COMPLEX1:13;
hence  (Re c) . n = Re (c . n) by A6; ::_thesis: verum
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
let c be FinSequence of COMPLEX ; ::_thesis: for n being Nat st n in dom (Im c) holds
(Im c) . n = Im (c . n)
let n be Nat; ::_thesis: ( n in dom (Im c) implies (Im c) . n = Im (c . n) )
assume A1: n in dom (Im c) ; ::_thesis: (Im c) . n = Im (c . n)
then A2: 1 <= n by FINSEQ_3:25;
 n <= len (Im c) by A1, FINSEQ_3:25;
then A3: n <= len c by COMPLSP2:48;
A4: ((- ((1 / 2) * <i>)) * (c *')) . n = (- ((1 / 2) * <i>)) * ((c *') . n) by COMPLSP2:16
.= (- ((1 / 2) * <i>)) * ((c . n) *') by A2, A3, COMPLSP2:def_1 ;
 ( len ((- ((1 / 2) * <i>)) * c) = len c & len ((- ((1 / 2) * <i>)) * (c *')) = len (c *') ) by COMPLSP2:3;
then A5: len ((- ((1 / 2) * <i>)) * c) = len ((- ((1 / 2) * <i>)) * (c *')) by COMPLSP2:def_1;
 len (c *') = len c by COMPLSP2:def_1;
then  ( n in NAT & (- ((1 / 2) * <i>)) * (c - (c *')) = ((- ((1 / 2) * <i>)) * c) - ((- ((1 / 2) * <i>)) * (c *')) ) by COMPLSP2:43, ORDINAL1:def_12;
then  (Im c) . n = (((- ((1 / 2) * <i>)) * c) . n) - (((- ((1 / 2) * <i>)) * (c *')) . n) by A5, COMPLSP2:25;
then A6: (Im c) . n = ((- ((1 / 2) * <i>)) * (c . n)) - ((- ((1 / 2) * <i>)) * ((c . n) *')) by A4, COMPLSP2:16;
 (c . n) - ((c . n) *') = ((Re (c . n)) + ((Im (c . n)) * <i>)) - ((Re (c . n)) - ((Im (c . n)) * <i>)) by COMPLEX1:13;
hence  (Im c) . n = Im (c . n) by A6; ::_thesis: verum
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
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, Def15;
 dom (Im f) = dom f by COMSEQ_3:def_4;
then A3: dom (Im f) = union (rng F) by A1, Def15;
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, Def15;
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, Def15;
 dom (Re f) = dom f by COMSEQ_3:def_3;
then A9: dom (Re f) = union (rng F) by A1, Def15;
 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, Def15;
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, Def14; ::_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, Def14;
A16: dom (Re f) = union (rng F) by A13, Def14;
then A17: dom f = union (rng F) by COMSEQ_3:def_3;
A18: dom F = dom (Im a) by A14, Def14;
A19: dom (Im f) = union (rng F) by A14, Def14;
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, Def14;
then A26: Im (f . x) = Im (a . n) by A18, A21, A24, Th47;
 (Re f) . x = (Re a) . n by A13, A21, A22, Def14;
then  Re (f . x) = Re (a . n) by A15, A21, A25, Th46;
hence  f . x = a . n by A26, COMPLEX1:def_3; ::_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, Def15; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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 ) ) )
let S be SigmaField of X; ::_thesis: 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 ) ) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( 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 ) ) )
hereby  ::_thesis: ( 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 ) ) implies f is_simple_func_in S )
assume  f is_simple_func_in S ; ::_thesis: 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 ) )
then consider F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX  such that
A1: F,c are_Re-presentation_of f by Th45;
 F, Im c are_Re-presentation_of Im f by A1, Th48;
then A2: 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 by Def14;
 F, Re c are_Re-presentation_of Re f by A1, Th48;
then A3: 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 by Def14;
 ( dom f = union (rng F) & dom F = dom c ) by A1, Def15;
hence  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 ) ) by A3, A2; ::_thesis: verum
end;
given F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX  such that A4: dom f = union (rng F) and
A5: dom F = dom c and
A6: 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 and
A7: 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 ; ::_thesis: f is_simple_func_in S
A8: dom (Im f) = union (rng F) by A4, COMSEQ_3:def_4;
 len (Im c) = len c by COMPLSP2:48;
then  dom (Im c) = Seg (len c) by FINSEQ_1:def_3;
then A9: dom F = dom (Im c) by A5, FINSEQ_1:def_3;
 len (Re c) = len c by COMPLSP2:48;
then  dom (Re c) = Seg (len c) by FINSEQ_1:def_3;
then A10: dom F = dom (Re c) by A5, FINSEQ_1:def_3;
A11: dom (Re f) = union (rng F) by A4, COMSEQ_3:def_3;
 for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = c . n
proof
let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds
f . x = c . n )
assume A12: n in dom F ; ::_thesis: for x being set st x in F . n holds
f . x = c . n
let x be set ; ::_thesis: ( x in F . n implies f . x = c . n )
assume A13: x in F . n ; ::_thesis: f . x = c . n
A14: F . n c= union (rng F) by A12, MESFUNC3:7;
then  x in dom (Im f) by A8, A13;
then A15: (Im f) . x = Im (f . x) by COMSEQ_3:def_4;
 x in dom (Re f) by A11, A13, A14;
then A16: (Re f) . x = Re (f . x) by COMSEQ_3:def_3;
 (Im f) . x = (Im c) . n by A7, A12, A13;
then A17: Im (f . x) = Im (c . n) by A9, A12, A15, Th47;
 (Re f) . x = (Re c) . n by A6, A12, A13;
then  Re (f . x) = Re (c . n) by A10, A12, A16, Th46;
hence  f . x = c . n by A17, COMPLEX1:def_3; ::_thesis: verum
end;
then  F,c are_Re-presentation_of f by A4, A5, Def15;
hence  f is_simple_func_in S by Th45; ::_thesis: verum
end;