mesfun7c.miz

begin

 reserve X for non empty set,

Y for set,

S for SigmaField of X,

M for sigma_Measure of S,

f,g for PartFunc of X, COMPLEX ,

r for Real,

k for Real,

n for Nat,

E for Element of S;

 definition

 let X be non empty set;

 let f be Functional_Sequence of X, REAL ;

 :: MESFUN7C:def1

 func R_EAL f -> Functional_Sequence of X, ExtREAL equals f;

 coherence

 proof

 ( dom f) = NAT & for n be Nat holds (f . n) is PartFunc of X, ExtREAL by NUMBERS: 31, RELSET_1: 7, SEQFUNC: 1;

 hence thesis by SEQFUNC: 1;

 end;

 end

 theorem :: MESFUN7C:1



 Th1: for X be non empty set, f be Functional_Sequence of X, REAL , x be Element of X holds (f # x) = (( R_EAL f) # x)

 proof

 let X be non empty set;

 let f be Functional_Sequence of X, REAL ;

 let x be Element of X;

 now

 let r be object;

 assume r in ( rng (( R_EAL f) # x));

 then

 consider n be object such that

 A1: n in NAT and

 A2: ((( R_EAL f) # x) . n) = r by FUNCT_2: 11;

 reconsider 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 by XREAL_0:def 1;

 end;

 then ( rng (( R_EAL f) # x)) c= REAL ;

 then

 reconsider RFx = (( R_EAL f) # x) as sequence of REAL by FUNCT_2: 6;

 reconsider RFx as Real_Sequence;

 now

 let n be object;

 assume n in NAT ;

 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;

 end;

 hence thesis by FUNCT_2: 12;

 end;

 registration

 let X be non empty set, f be Function of X, REAL ;

 cluster ( R_EAL f) -> total;

 coherence ;

 end

 definition

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

 :: MESFUN7C:def2

 func inf f -> PartFunc of X, ExtREAL equals ( inf ( R_EAL f));

 coherence ;

 end

 theorem :: MESFUN7C:2



 Th2: for X be non empty set, f be Functional_Sequence of X, REAL holds for x be 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, f be Functional_Sequence of X, REAL ;

 let x be Element of X;

 assume x in ( dom ( inf f));

 then (( inf f) . x) = ( inf (( R_EAL f) # x)) by MESFUNC8:def 3;

 hence thesis by Th1;

 end;

 definition

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

 :: MESFUN7C:def3

 func sup f -> PartFunc of X, ExtREAL equals ( sup ( R_EAL f));

 coherence ;

 end

 theorem :: MESFUN7C:3



 Th3: for X be non empty set, f be Functional_Sequence of X, REAL holds for x be 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, f be Functional_Sequence of X, REAL ;

 let x be Element of X;

 assume x in ( dom ( sup f));

 then (( sup f) . x) = ( sup (( R_EAL f) # x)) by MESFUNC8:def 4;

 hence thesis by Th1;

 end;

 definition

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

 :: MESFUN7C:def4

 func inferior_realsequence f -> with_the_same_dom Functional_Sequence of X, ExtREAL equals ( inferior_realsequence ( R_EAL f));

 coherence ;

 end

 theorem :: MESFUN7C:4



 Th4: for X be non empty set, f be Functional_Sequence of X, REAL , n be Nat holds ( dom (( inferior_realsequence f) . n)) = ( dom (f . 0 )) & for x be 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;

 let f be Functional_Sequence of X, REAL ;

 let n be Nat;

 set IF = ( inferior_realsequence f);

 ( dom (IF . n)) = ( dom (( R_EAL f) . 0 )) by MESFUNC8:def 5

 .= ( dom ( R_EAL (f . 0 )));

 hence ( dom (( inferior_realsequence f) . n)) = ( dom (f . 0 ));

 hereby

 let x be Element of X;

 assume x in ( dom (IF . n));



 then

 A1: ((IF . n) . x) = (( inferior_realsequence (( R_EAL f) # x)) . n) by MESFUNC8:def 5

 .= ( inf ((( R_EAL f) # x) ^\ n)) by RINFSUP2: 27;

 (( R_EAL f) # x) = (f # x) by Th1;

 hence ((IF . n) . x) = (( inferior_realsequence ( R_EAL (f # x))) . n) by A1, RINFSUP2: 27;

 end;

 end;

 definition

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

 :: MESFUN7C:def5

 func superior_realsequence f -> with_the_same_dom Functional_Sequence of X, ExtREAL equals ( superior_realsequence ( R_EAL f));

 coherence ;

 end

 theorem :: MESFUN7C:5



 Th5: for X be non empty set, f be Functional_Sequence of X, REAL , n be Nat holds ( dom (( superior_realsequence f) . n)) = ( dom (f . 0 )) & for x be 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;

 let f be Functional_Sequence of X, REAL ;

 let n be Nat;

 set SF = ( superior_realsequence f);

 thus ( dom (( superior_realsequence f) . n)) = ( dom (f . 0 )) by MESFUNC8:def 6;

 hereby

 let x be Element of X;

 assume x in ( dom (SF . n));

 then ((SF . n) . x) = (( superior_realsequence (( R_EAL f) # x)) . n) by MESFUNC8:def 6;

 hence ((SF . n) . x) = (( superior_realsequence ( R_EAL (f # x))) . n) by Th1;

 end;

 end;

 theorem :: MESFUN7C:6

 for f be Functional_Sequence of X, REAL , x be Element of X st x in ( dom (f . 0 )) holds (( inferior_realsequence f) # x) = ( inferior_realsequence ( R_EAL (f # x)))

 proof

 let f be Functional_Sequence of X, REAL ;

 let x be Element of X;

 set F = ( inferior_realsequence f);

 assume

 A1: x in ( dom (f . 0 ));

 now

 let n be Element of NAT ;

 ( dom (F . n)) = ( dom (f . 0 )) & ((F # x) . n) = ((F . n) . x) by Th4, MESFUNC5:def 13;

 hence ((F # x) . n) = (( inferior_realsequence ( R_EAL (f # x))) . n) by A1, Th4;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 registration

 let X be non empty set, f be with_the_same_dom Functional_Sequence of X, REAL ;

 cluster ( R_EAL f) -> with_the_same_dom;

 coherence

 proof

 for n,m be Nat holds ( dom (( R_EAL f) . n)) = ( dom (( R_EAL f) . m)) by MESFUNC8:def 2;

 hence thesis by MESFUNC8:def 2;

 end;

 end

 theorem :: MESFUN7C:7



 Th7: for X be non empty set, f be with_the_same_dom Functional_Sequence of X, REAL holds for S be SigmaField of X, E be Element of S, n be Nat st (f . n) is E -measurable holds (( R_EAL f) . n) is E -measurable

 proof

 let X be non empty set, f be with_the_same_dom Functional_Sequence of X, REAL ;

 let S be SigmaField of X, E be Element of S, n be Nat;

 assume (f . n) is E -measurable;

 then ( R_EAL (f . n)) is E -measurable by MESFUNC6:def 1;

 hence thesis;

 end;

 theorem :: MESFUN7C:8

 for X be non empty set, f be Functional_Sequence of X, REAL , n be Nat holds (( R_EAL f) ^\ n) = ( R_EAL (f ^\ n));

 theorem :: MESFUN7C:9

 for f be with_the_same_dom Functional_Sequence of X, REAL , n be Nat holds (( inferior_realsequence f) . n) = ( inf (f ^\ n))

 proof

 let f be with_the_same_dom Functional_Sequence of X, REAL , n be Nat;

 n in NAT by ORDINAL1:def 12;

 then (( inferior_realsequence ( R_EAL f)) . n) = ( inf (( R_EAL f) ^\ n)) by MESFUNC8: 8;

 hence thesis;

 end;

 theorem :: MESFUN7C:10

 for f be with_the_same_dom Functional_Sequence of X, REAL , n be Nat holds (( superior_realsequence f) . n) = ( sup (f ^\ n))

 proof

 let f be with_the_same_dom Functional_Sequence of X, REAL , n be Nat;

 n in NAT by ORDINAL1:def 12;

 then (( superior_realsequence ( R_EAL f)) . n) = ( sup (( R_EAL f) ^\ n)) by MESFUNC8: 9;

 hence thesis;

 end;

 theorem :: MESFUN7C:11



 Th11: for f be Functional_Sequence of X, REAL , x be Element of X st x in ( dom (f . 0 )) holds (( superior_realsequence f) # x) = ( superior_realsequence ( R_EAL (f # x)))

 proof

 let f be Functional_Sequence of X, REAL , x be Element of X;

 set F = ( superior_realsequence f);

 assume

 A1: x in ( dom (f . 0 ));

 now

 let n be Element of NAT ;

 ( dom (F . n)) = ( dom (f . 0 )) & ((F # x) . n) = ((F . n) . x) by Th5, MESFUNC5:def 13;

 hence ((F # x) . n) = (( superior_realsequence ( R_EAL (f # x))) . n) by A1, Th5;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 definition

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

 :: MESFUN7C:def6

 func lim_inf f -> PartFunc of X, ExtREAL equals ( lim_inf ( R_EAL f));

 coherence ;

 end

 theorem :: MESFUN7C:12



 Th12: for X be non empty set, f be Functional_Sequence of X, REAL holds for x be 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, f be Functional_Sequence of X, REAL ;

 let x be Element of X;

 assume x in ( dom ( lim_inf f));

 then (( lim_inf f) . x) = ( lim_inf (( R_EAL f) # x)) by MESFUNC8:def 7;

 hence thesis by Th1;

 end;

 definition

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

 :: MESFUN7C:def7

 func lim_sup f -> PartFunc of X, ExtREAL equals ( lim_sup ( R_EAL f));

 coherence ;

 end

 theorem :: MESFUN7C:13



 Th13: for X be non empty set, f be Functional_Sequence of X, REAL holds for x be 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, f be Functional_Sequence of X, REAL ;

 let x be Element of X;

 assume x in ( dom ( lim_sup f));

 then (( lim_sup f) . x) = ( lim_sup (( R_EAL f) # x)) by MESFUNC8:def 8;

 hence thesis by Th1;

 end;

 definition

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

 :: MESFUN7C:def8

 func lim f -> PartFunc of X, ExtREAL equals ( lim ( R_EAL f));

 coherence ;

 end

 theorem :: MESFUN7C:14



 Th14: for X be non empty set, f be Functional_Sequence of X, REAL holds for x be 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, f be Functional_Sequence of X, REAL ;

 let x be Element of X;

 assume x in ( dom ( lim f));

 then (( lim f) . x) = ( lim (( R_EAL f) # x)) by MESFUNC8:def 9;

 hence thesis by Th1;

 end;

 theorem :: MESFUN7C:15



 Th15: for f be Functional_Sequence of X, REAL , x be 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 f be Functional_Sequence of X, REAL ;

 let x be Element of X;

 assume that

 A1: x in ( dom ( lim f)) and

 A2: (f # x) is convergent;

 ( 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 thesis by A1, A5, A3, Th14;

 end;

 theorem :: MESFUN7C:16

 for f be with_the_same_dom Functional_Sequence of X, REAL , F be SetSequence of S, r be Real st (for n be 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 f be with_the_same_dom Functional_Sequence of X, REAL , F be SetSequence of S, r be Real;

 set E = ( dom (f . 0 ));

 assume

 A1: for n be Nat holds (F . n) = (E /\ ( great_dom ((f . n),r)));

 now

 let x be object;

 assume

 A2: x in (E /\ ( great_dom (( sup f),r)));

 then

 reconsider z = x as Element of X;



 A3: x in E 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 be Element of NAT st r < ((f # z) . n)

 proof

 assume

 A5: for n be Element of NAT holds ((f # z) . n) <= r;

 for p be ExtReal holds p in ( rng ( R_EAL (f # z))) implies p <= r

 proof

 let p be ExtReal;

 assume p in ( rng ( R_EAL (f # z)));

 then ex n be object st n in NAT & (( R_EAL (f # z)) . n) = p by FUNCT_2: 11;

 hence thesis by A5;

 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;

 end;

 then

 consider n be 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) = (E /\ ( 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;

 end;

 then

 A11: (E /\ ( great_dom (( sup f),r))) c= ( union ( rng F));

 now

 let x be object;

 assume x in ( union ( rng F));

 then

 consider y be set such that

 A12: x in y and

 A13: y in ( rng F qua SetSequence of X) by TARSKI:def 4;

 reconsider z = x as Element of X by A12, A13;

 consider n be object such that

 A14: n in ( dom F) and

 A15: y = (F . n) by A13, FUNCT_1:def 3;

 reconsider n as Element of NAT by A14;



 A16: (F . n) = (E /\ ( 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 E 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 (E /\ ( great_dom (( sup f),r))) by A19, XBOOLE_0:def 4;

 end;

 then ( union ( rng F)) c= (E /\ ( great_dom (( sup f),r)));

 hence thesis by A11;

 end;

 theorem :: MESFUN7C:17

 for f be with_the_same_dom Functional_Sequence of X, REAL , F be SetSequence of S, r be Real st (for n be 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 f be with_the_same_dom Functional_Sequence of X, REAL , F be SetSequence of S, r be Real;

 set E = ( dom (f . 0 ));

 assume

 A1: for n be Nat holds (F . n) = (( dom (f . 0 )) /\ ( great_eq_dom ((f . n),r)));

 now

 let x be object;

 assume

 A2: x in ( meet ( rng F qua SetSequence of X));

 then

 reconsider z = x as Element of X;



 A3: (F . 0 ) = (E /\ ( 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 E by A3, XBOOLE_0:def 4;

 then

 A5: x in ( dom ( inf f)) by MESFUNC8:def 3;

 A6:

 now

 let n be Element of NAT ;

 (F . n) in ( rng F) by FUNCT_2: 4;

 then

 A7: z in (F . n) by A2, SETFAM_1:def 1;

 (F . n) = (E /\ ( 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;

 end;

 for p be ExtReal holds p in ( rng ( R_EAL (f # z))) implies r <= p

 proof

 let p be ExtReal;

 assume p in ( rng ( R_EAL (f # z)));

 then ex n be object st n in NAT & (( R_EAL (f # z)) . n) = p by FUNCT_2: 11;

 hence thesis by A6;

 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 (E /\ ( great_eq_dom (( inf f),r))) by A4, XBOOLE_0:def 4;

 end;

 then

 A8: ( meet ( rng F)) c= (E /\ ( great_eq_dom (( inf f),r)));

 now

 let x be object;

 assume

 A9: x in (E /\ ( great_eq_dom (( inf f),r)));

 then

 reconsider z = x as Element of X;



 A10: x in E 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

 let y be set;

 assume y in ( rng F);

 then

 consider n be object such that

 A12: n in NAT and

 A13: y = (F . n) by FUNCT_2: 11;

 reconsider 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) = (E /\ ( great_eq_dom ((f . n),r))) by A1;

 hence x in y by A10, A13, A16, XBOOLE_0:def 4;

 end;

 hence x in ( meet ( rng F)) by SETFAM_1:def 1;

 end;

 then (E /\ ( great_eq_dom (( inf f),r))) c= ( meet ( rng F));

 hence thesis by A8;

 end;

 theorem :: MESFUN7C:18



 Th18: for f be with_the_same_dom Functional_Sequence of X, REAL , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) holds ( lim_sup f) is E -measurable

 proof

 let f be with_the_same_dom Functional_Sequence of X, REAL , E be Element of S;

 assume that

 A1: ( dom (f . 0 )) = E and

 A2: for n be Nat holds (f . n) is E -measurable;

 for n be Nat holds (( R_EAL f) . n) is E -measurable

 proof

 let n be Nat;

 (f . n) is E -measurable by A2;

 hence thesis by Th7;

 end;

 hence thesis by A1, MESFUNC8: 23;

 end;

 theorem :: MESFUN7C:19

 for f be with_the_same_dom Functional_Sequence of X, REAL , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) holds ( lim_inf f) is E -measurable

 proof

 let f be with_the_same_dom Functional_Sequence of X, REAL , E be Element of S;

 assume that

 A1: ( dom (f . 0 )) = E and

 A2: for n be Nat holds (f . n) is E -measurable;

 for n be Nat holds (( R_EAL f) . n) is E -measurable

 proof

 let n be Nat;

 (f . n) is E -measurable by A2;

 hence thesis by Th7;

 end;

 hence thesis by A1, MESFUNC8: 24;

 end;

 theorem :: MESFUN7C:20

 for f be Functional_Sequence of X, REAL , x be Element of X st x in ( dom (f . 0 )) & (f # x) is convergent holds (( superior_realsequence f) # x) is bounded_below

 proof

 let f be Functional_Sequence of X, REAL , x be Element of X;

 assume

 A1: x in ( dom (f . 0 ));

 assume (f # x) is convergent;

 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 thesis by A3, RINFSUP2: 13;

 end;

 theorem :: MESFUN7C:21



 Th21: for f be with_the_same_dom Functional_Sequence of X, REAL , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) & (for x be Element of X st x in E holds (f # x) is convergent) holds ( lim f) is E -measurable

 proof

 let f be with_the_same_dom Functional_Sequence of X, REAL , E be Element of S;

 assume

 A1: ( dom (f . 0 )) = E;

 then

 A2: ( dom ( lim f)) = E by MESFUNC8:def 9;

 assume for n be Nat holds (f . n) is E -measurable;

 then

 A3: ( lim_sup f) is E -measurable by A1, Th18;

 assume

 A4: for x be Element of X st x in E holds (f # x) is convergent;

 A5:

 now

 let x be Element of X;

 assume

 A6: x in ( dom ( lim f));

 then (f # x) is convergent by A2, A4;

 hence (( lim f) . x) = (( lim_sup f) . x) by A6, Th15;

 end;

 ( dom ( lim_sup f)) = E by A1, MESFUNC8:def 8;

 hence thesis by A2, A3, A5, PARTFUN1: 5;

 end;

 theorem :: MESFUN7C:22



 Th22: for f be with_the_same_dom Functional_Sequence of X, REAL , g be PartFunc of X, ExtREAL , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) & ( dom g) = E & for x be Element of X st x in E holds (f # x) is convergent & (g . x) = ( lim (f # x)) holds g is E -measurable

 proof

 let f be with_the_same_dom Functional_Sequence of X, REAL , g be PartFunc of X, ExtREAL , E be Element of S;

 assume that

 A1: ( dom (f . 0 )) = E and

 A2: for n be Nat holds (f . n) is E -measurable and

 A3: ( dom g) = E and

 A4: for x be Element of X st x in E holds (f # x) is convergent & (g . x) = ( lim (f # x));



 A5: ( dom ( lim f)) = E by A1, MESFUNC8:def 9;

 now

 let x be Element of X;

 assume

 A6: x in ( dom ( lim f));

 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;

 end;

 then

 A7: g = ( lim f) by A3, A5, PARTFUN1: 5;

 for x be Element of X st x in E holds (f # x) is convergent by A4;

 hence thesis by A1, A2, A7, Th21;

 end;

 begin

 definition

 let X be non empty set, H be Functional_Sequence of X, COMPLEX , x be Element of X;

 :: MESFUN7C:def9

 func H # x -> Complex_Sequence means

 : Def9: for n be Nat holds (it . n) = ((H . n) . x);

 existence

 proof

 defpred P[ Element of NAT , set] means $2 = ((H . $1) . x);



 A1: for n be Element of NAT holds ex y be Element of COMPLEX st P[n, y]

 proof

 let n be Element of NAT ;

 ((H . n) . x) in COMPLEX by XCMPLX_0:def 2;

 hence thesis;

 end;

 consider f be sequence of COMPLEX such that

 A2: for n be Element of NAT holds P[n, (f . n)] from FUNCT_2:sch 3( A1);

 take f;

 let n be Nat;

 n in NAT by ORDINAL1:def 12;

 hence thesis by A2;

 end;

 uniqueness

 proof

 let S1,S2 be Complex_Sequence such that

 A3: for n be Nat holds (S1 . n) = ((H . n) . x) and

 A4: for n be Nat holds (S2 . n) = ((H . n) . x);

 now

 let n be Element of NAT ;

 (S1 . n) = ((H . n) . x) by A3;

 hence (S1 . n) = (S2 . n) by A4;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 end

 definition

 let X be non empty set, f be Functional_Sequence of X, COMPLEX ;

 :: MESFUN7C:def10

 func lim f -> PartFunc of X, COMPLEX means

 : Def10: ( dom it ) = ( dom (f . 0 )) & for x be Element of X st x in ( dom it ) holds (it . x) = ( lim (f # x));

 existence

 proof

 defpred P[ set] means $1 in ( dom (f . 0 ));

 deffunc F( Element of X) = ( In (( lim (f # $1)), COMPLEX ));

 consider g be PartFunc of X, COMPLEX such that

 A1: (for x be Element of X holds x in ( dom g) iff P[x]) & for x be Element of X st x in ( dom g) holds (g /. x) = F(x) from PARTFUN2:sch 2;

 take g;

 A2:

 now

 let x be Element of X;

 assume

 A3: x in ( dom g);

 then (g /. x) = F(x) by A1;

 hence (g . x) = ( lim (f # x)) by A3, PARTFUN1:def 6;

 end;

 for x be object holds x in ( dom g) iff x in ( dom (f . 0 )) by A1;

 hence thesis by A2, TARSKI: 2;

 end;

 uniqueness

 proof

 let g,h be PartFunc of X, COMPLEX ;

 assume that

 A4: ( dom g) = ( dom (f . 0 )) and

 A5: for x be Element of X st x in ( dom g) holds (g . x) = ( lim (f # x));

 assume that

 A6: ( dom h) = ( dom (f . 0 )) and

 A7: for x be Element of X st x in ( dom h) holds (h . x) = ( lim (f # x));

 now

 let x be Element of X;

 assume

 A8: x in ( dom g);

 then (g . x) = ( lim (f # x)) by A5;

 hence (g . x) = (h . x) by A4, A6, A7, A8;

 end;

 hence thesis by A4, A6, PARTFUN1: 5;

 end;

 end

 definition

 let X be non empty set;

 let f be Functional_Sequence of X, COMPLEX ;

 :: MESFUN7C:def11

 func Re f -> Functional_Sequence of X, REAL means

 : Def11: for n be Nat holds ( dom (it . n)) = ( dom (f . n)) & for x be Element of X st x in ( dom (it . n)) holds ((it . n) . x) = (( Re (f # x)) . n);

 existence

 proof

 defpred P[ Element of NAT , Function] means ( dom $2) = ( dom (f . $1)) & for x be Element of X st x in ( dom $2) holds ($2 . x) = (( Re (f # x)) . $1);



 A1: for n be Element of NAT holds ex y be Element of ( PFuncs (X, REAL )) st P[n, y]

 proof

 let n be Element of NAT ;

 deffunc F( Element of X) = ( In ((( Re (f # $1)) . n), REAL ));

 defpred P[ set] means $1 in ( dom (f . n));

 consider g be PartFunc of X, REAL such that

 A2: (for x be Element of X holds x in ( dom g) iff P[x]) & for x be Element of X st x in ( dom g) holds (g /. x) = F(x) from PARTFUN2:sch 2;

 take g;

 A3:

 now

 let x be Element of X;

 assume

 A4: x in ( dom g);



 then (g /. x) = F(x) by A2

 .= (( Re (f # x)) . n);

 hence (g . x) = (( Re (f # x)) . n) by A4, PARTFUN1:def 6;

 end;

 for x be object holds x in ( dom g) iff x in ( dom (f . n)) by A2;

 hence thesis by A3, PARTFUN1: 45, TARSKI: 2;

 end;

 consider g be sequence of ( PFuncs (X, REAL )) such that

 A5: for n be Element of NAT holds P[n, (g . n)] from FUNCT_2:sch 3( A1);

 reconsider g as Functional_Sequence of X, REAL ;

 take g;

 thus for n holds ( dom (g . n)) = ( dom (f . n)) & for x be Element of X st x in ( dom (g . n)) holds ((g . n) . x) = (( Re (f # x)) . n)

 proof

 let n;

 n in NAT by ORDINAL1:def 12;

 hence thesis by A5;

 end;

 end;

 uniqueness

 proof

 let g,h be Functional_Sequence of X, REAL ;

 assume

 A6: for n holds ( dom (g . n)) = ( dom (f . n)) & for x be Element of X st x in ( dom (g . n)) holds ((g . n) . x) = (( Re (f # x)) . n);

 assume

 A7: for n holds ( dom (h . n)) = ( dom (f . n)) & for x be Element of X st x in ( dom (h . n)) holds ((h . n) . x) = (( Re (f # x)) . n);

 now

 let n be Element of NAT ;



 A8: ( dom (g . n)) = ( dom (f . n)) by A6

 .= ( dom (h . n)) by A7;

 now

 let x be Element of X;

 assume

 A9: x in ( dom (g . n));

 then ((g . n) . x) = (( Re (f # x)) . n) by A6;

 hence ((g . n) . x) = ((h . n) . x) by A7, A8, A9;

 end;

 hence (g . n) = (h . n) by A8, PARTFUN1: 5;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 end

 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

 proof

 now

 let k,l be Nat;

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

 end;

 hence thesis by MESFUNC8:def 2;

 end;

 end

 definition

 let X be non empty set;

 let f be Functional_Sequence of X, COMPLEX ;

 :: MESFUN7C:def12

 func Im f -> Functional_Sequence of X, REAL means

 : Def12: for n be Nat holds ( dom (it . n)) = ( dom (f . n)) & for x be Element of X st x in ( dom (it . n)) holds ((it . n) . x) = (( Im (f # x)) . n);

 existence

 proof

 defpred P[ Element of NAT , Function] means ( dom $2) = ( dom (f . $1)) & for x be Element of X st x in ( dom $2) holds ($2 . x) = (( Im (f # x)) . $1);



 A1: for n be Element of NAT holds ex y be Element of ( PFuncs (X, REAL )) st P[n, y]

 proof

 let n be Element of NAT ;

 deffunc F( Element of X) = ( In ((( Im (f # $1)) . n), REAL ));

 defpred P[ set] means $1 in ( dom (f . n));

 consider g be PartFunc of X, REAL such that

 A2: (for x be Element of X holds x in ( dom g) iff P[x]) & for x be Element of X st x in ( dom g) holds (g /. x) = F(x) from PARTFUN2:sch 2;

 take g;

 A3:

 now

 let x be Element of X;

 assume

 A4: x in ( dom g);



 then (g /. x) = F(x) by A2

 .= (( Im (f # x)) . n);

 hence (g . x) = (( Im (f # x)) . n) by A4, PARTFUN1:def 6;

 end;

 for x be object holds x in ( dom g) iff x in ( dom (f . n)) by A2;

 hence thesis by A3, PARTFUN1: 45, TARSKI: 2;

 end;

 consider g be sequence of ( PFuncs (X, REAL )) such that

 A5: for n be Element of NAT holds P[n, (g . n)] from FUNCT_2:sch 3( A1);

 reconsider g as Functional_Sequence of X, REAL ;

 take g;

 thus for n holds ( dom (g . n)) = ( dom (f . n)) & for x be Element of X st x in ( dom (g . n)) holds ((g . n) . x) = (( Im (f # x)) . n)

 proof

 let n;

 n in NAT by ORDINAL1:def 12;

 hence thesis by A5;

 end;

 end;

 uniqueness

 proof

 let g,h be Functional_Sequence of X, REAL ;

 assume

 A6: for n holds ( dom (g . n)) = ( dom (f . n)) & for x be Element of X st x in ( dom (g . n)) holds ((g . n) . x) = (( Im (f # x)) . n);

 assume

 A7: for n holds ( dom (h . n)) = ( dom (f . n)) & for x be Element of X st x in ( dom (h . n)) holds ((h . n) . x) = (( Im (f # x)) . n);

 now

 let n be Element of NAT ;



 A8: ( dom (g . n)) = ( dom (f . n)) by A6

 .= ( dom (h . n)) by A7;

 now

 let x be Element of X;

 assume

 A9: x in ( dom (g . n));

 then ((g . n) . x) = (( Im (f # x)) . n) by A6;

 hence ((g . n) . x) = ((h . n) . x) by A7, A8, A9;

 end;

 hence (g . n) = (h . n) by A8, PARTFUN1: 5;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 end

 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

 proof

 now

 let k,l be Nat;

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

 end;

 hence thesis by MESFUNC8:def 2;

 end;

 end

 theorem :: MESFUN7C:23



 Th23: for f be with_the_same_dom Functional_Sequence of X, COMPLEX , x be Element of X st x in ( dom (f . 0 )) holds (( Re f) # x) = ( Re (f # x)) & (( Im f) # x) = ( Im (f # x))

 proof

 let f be with_the_same_dom Functional_Sequence of X, COMPLEX ;

 let x be Element of X;

 set F = ( Re f);

 set G = ( Im f);

 assume

 A1: x in ( dom (f . 0 ));

 now

 let n be Element of NAT ;

 ( dom (F . n)) = ( dom (f . n)) by Def11;

 then

 A2: ( dom (F . n)) = ( dom (f . 0 )) by MESFUNC8:def 2;

 ( dom (G . n)) = ( dom (f . n)) by Def12;

 then

 A3: ( dom (G . n)) = ( dom (f . 0 )) by MESFUNC8:def 2;

 ((F # x) . n) = ((F . n) . x) & ((G # x) . n) = ((G . n) . x) by SEQFUNC:def 10;

 hence ((F # x) . n) = (( Re (f # x)) . n) & ((G # x) . n) = (( Im (f # x)) . n) by A1, A2, A3, Def11, Def12;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: MESFUN7C:24



 Th24: for f be Functional_Sequence of X, COMPLEX , n be Nat holds (( Re f) . n) = ( Re (f . n)) & (( Im f) . n) = ( Im (f . n))

 proof

 let f be Functional_Sequence of X, COMPLEX ;

 let n be Nat;

 ( dom (( Re f) . n)) = ( dom (f . n)) by Def11;

 then

 A1: ( dom (( Re f) . n)) = ( dom ( Re (f . n))) by COMSEQ_3:def 3;

 now

 let x be Element of X;

 assume

 A2: x in ( dom (( Re f) . n));

 then (( Re (f . n)) . x) = ( Re ((f . n) . x)) by A1, COMSEQ_3:def 3;

 then

 A3: (( Re (f . n)) . x) = ( Re ((f # x) . n)) by Def9;

 ((( Re f) . n) . x) = (( Re (f # x)) . n) by A2, Def11;

 hence ((( Re f) . n) . x) = (( Re (f . n)) . x) by A3, COMSEQ_3:def 5;

 end;

 hence (( Re f) . n) = ( Re (f . n)) by A1, PARTFUN1: 5;

 ( dom (( Im f) . n)) = ( dom (f . n)) by Def12;

 then

 A4: ( dom (( Im f) . n)) = ( dom ( Im (f . n))) by COMSEQ_3:def 4;

 now

 let x be Element of X;

 assume

 A5: x in ( dom (( Im f) . n));

 then (( Im (f . n)) . x) = ( Im ((f . n) . x)) by A4, COMSEQ_3:def 4;

 then

 A6: (( Im (f . n)) . x) = ( Im ((f # x) . n)) by Def9;

 ((( Im f) . n) . x) = (( Im (f # x)) . n) by A5, Def12;

 hence ((( Im f) . n) . x) = (( Im (f . n)) . x) by A6, COMSEQ_3:def 6;

 end;

 hence thesis by A4, PARTFUN1: 5;

 end;

 theorem :: MESFUN7C:25



 Th25: for f be with_the_same_dom Functional_Sequence of X, COMPLEX st (for x be 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 f be with_the_same_dom Functional_Sequence of X, COMPLEX ;

 ( 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 be Element of X st x in ( dom (f . 0 )) holds (f # x) is convergent;

 A5:

 now

 let x be Element of X;

 assume

 A6: x in ( dom ( lim ( Re f)));

 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;

 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;

 ( 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

 let x be Element of X;

 assume

 A14: x in ( dom ( lim ( Im f)));

 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;

 end;

 ( Im ( lim f)) is PartFunc of X, ExtREAL by NUMBERS: 31, RELSET_1: 7;

 hence thesis by A12, A13, PARTFUN1: 5;

 end;

 theorem :: MESFUN7C:26

 for f be with_the_same_dom Functional_Sequence of X, COMPLEX , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) & (for x be Element of X st x in E holds (f # x) is convergent) holds ( lim f) is E -measurable

 proof

 let f be with_the_same_dom Functional_Sequence of X, COMPLEX , E be Element of S;

 assume that

 A1: ( dom (f . 0 )) = E and

 A2: for n be Nat holds (f . n) is E -measurable and

 A3: for x be Element of X st x in E holds (f # x) is convergent;



 A4: ( lim ( Im f)) = ( R_EAL ( Im ( lim f))) by A1, A3, Th25;

 A5:

 now

 let x be Element of X;

 assume

 A6: x in E;

 then (f # x) is convergent by A3;

 then ( Im (f # x)) is convergent;

 hence (( Im f) # x) is convergent by A1, A6, Th23;

 end;

 A7:

 now

 let n be Nat;

 (f . n) is E -measurable by A2;

 then ( Im (f . n)) is E -measurable by MESFUN6C:def 1;

 hence (( Im f) . n) is E -measurable by Th24;

 end;

 ( dom (( Im f) . 0 )) = E by A1, Def12;

 then ( lim ( Im f)) is E -measurable by A7, A5, Th21;

 then

 A8: ( Im ( lim f)) is E -measurable by A4, MESFUNC6:def 1;

 A9:

 now

 let x be Element of X;

 assume

 A10: x in E;

 then (f # x) is convergent by A3;

 then ( Re (f # x)) is convergent;

 hence (( Re f) # x) is convergent by A1, A10, Th23;

 end;

 A11:

 now

 let n be Nat;

 (f . n) is E -measurable by A2;

 then ( Re (f . n)) is E -measurable by MESFUN6C:def 1;

 hence (( Re f) . n) is E -measurable by Th24;

 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 E -measurable by A11, A9, Th21;

 then ( Re ( lim f)) is E -measurable by A12, MESFUNC6:def 1;

 hence thesis by A8, MESFUN6C:def 1;

 end;

 theorem :: MESFUN7C:27

 for f be with_the_same_dom Functional_Sequence of X, COMPLEX , g be PartFunc of X, COMPLEX , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) & ( dom g) = E & for x be Element of X st x in E holds (f # x) is convergent & (g . x) = ( lim (f # x)) holds g is E -measurable

 proof

 let f be with_the_same_dom Functional_Sequence of X, COMPLEX , g be PartFunc of X, COMPLEX , E be Element of S;

 assume that

 A1: ( dom (f . 0 )) = E and

 A2: for n be Nat holds (f . n) is E -measurable and

 A3: ( dom g) = E and

 A4: for x be Element of X st x in E holds (f # x) is convergent & (g . x) = ( lim (f # x));

 A5:

 now

 let n be Nat;

 (f . n) is E -measurable by A2;

 then ( Im (f . n)) is E -measurable by MESFUN6C:def 1;

 hence (( Im f) . n) is E -measurable by Th24;

 end;



 A6: ( dom ( Im g)) = E by A3, COMSEQ_3:def 4;

 A7:

 now

 let x be Element of X;

 assume

 A8: x in E;

 then

 A9: (f # x) is convergent by A4;

 then ( Im (f # x)) is convergent;

 hence (( Im f) # x) is convergent by A1, A8, Th23;

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

 end;

 ( dom (( Im f) . 0 )) = E by A1, Def12;

 then ( R_EAL ( Im g)) is E -measurable by A5, A6, A7, Th22;

 then

 A10: ( Im g) is E -measurable by MESFUNC6:def 1;

 A11:

 now

 let n be Nat;

 (f . n) is E -measurable by A2;

 then ( Re (f . n)) is E -measurable by MESFUN6C:def 1;

 hence (( Re f) . n) is E -measurable by Th24;

 end;



 A12: ( dom ( Re g)) = E by A3, COMSEQ_3:def 3;

 A13:

 now

 let x be Element of X;

 assume

 A14: x in E;

 then

 A15: (f # x) is convergent by A4;

 then ( Re (f # x)) is convergent;

 hence (( Re f) # x) is convergent by A1, A14, Th23;

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

 end;

 ( dom (( Re f) . 0 )) = E by A1, Def11;

 then ( R_EAL ( Re g)) is E -measurable by A11, A12, A13, Th22;

 then ( Re g) is E -measurable by MESFUNC6:def 1;

 hence thesis by A10, MESFUN6C:def 1;

 end;

 begin

 theorem :: MESFUN7C:28

 ((r (#) f) | Y) = (r (#) (f | Y))

 proof



 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

 let x be Element of X;

 assume

 A4: x in ( dom ((r (#) f) | Y));

 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;

 end;

 hence thesis by A3, PARTFUN1: 5;

 end;



 Lm1: |.f.| is nonnegative

 proof

 now

 let x be object;

 assume x in ( dom |.f.|);

 then ( |.f.| . x) = |.(f . x).| by VALUED_1:def 11;

 hence 0 <= ( |.f.| . x) by COMPLEX1: 46;

 end;

 hence thesis by MESFUNC6: 52;

 end;

 theorem :: MESFUN7C:29

 0 <= k & E c= ( dom f) & f is E -measurable implies ( |.f.| to_power k) is E -measurable

 proof

 assume that

 A1: 0 <= k and

 A2: E c= ( dom f) and

 A3: f is E -measurable;



 A4: |.f.| is nonnegative by Lm1;

 E c= ( dom |.f.|) by A2, VALUED_1:def 11;

 hence thesis by A1, A2, A3, A4, MESFUN6C: 29, MESFUN6C: 30;

 end;

 theorem :: MESFUN7C:30



 Th30: for f,g be PartFunc of X, REAL holds (( R_EAL f) (#) ( R_EAL g)) = ( R_EAL (f (#) g))

 proof

 let f,g be PartFunc of X, REAL ;



 A1: ( dom (( R_EAL f) (#) ( R_EAL g))) = (( dom ( R_EAL f)) /\ ( dom ( R_EAL g))) by MESFUNC1:def 5;

 A2:

 now

 let x be Element of X;

 assume

 A3: x in ( dom (( R_EAL f) (#) ( R_EAL g)));

 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;

 end;

 ( dom (( R_EAL f) (#) ( R_EAL g))) = ( dom ( R_EAL (f (#) g))) by A1, VALUED_1:def 4;

 hence thesis by A2, PARTFUN1: 5;

 end;

 theorem :: MESFUN7C:31



 Th31: for f,g be PartFunc of X, REAL st (( dom f) /\ ( dom g)) = E & f is E -measurable & g is E -measurable holds (f (#) g) is E -measurable

 proof

 let f,g be PartFunc of X, REAL ;

 assume that

 A1: (( dom f) /\ ( dom g)) = E and

 A2: f is E -measurable & g is E -measurable;

 ( R_EAL f) is E -measurable & ( R_EAL g) is E -measurable by A2, MESFUNC6:def 1;

 then (( R_EAL f) (#) ( R_EAL g)) is E -measurable by A1, MESFUNC7: 15;

 then ( R_EAL (f (#) g)) is E -measurable by Th30;

 hence thesis by MESFUNC6:def 1;

 end;

 theorem :: MESFUN7C:32



 Th32: ( Re (f (#) g)) = ((( Re f) (#) ( Re g)) - (( Im f) (#) ( Im g))) & ( Im (f (#) g)) = ((( Im f) (#) ( Re g)) + (( Re f) (#) ( Im g)))

 proof



 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

 let x be object;

 assume

 A10: x in ( dom ( Re (f (#) g)));

 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;

 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;



 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

 let x be object;

 assume

 A18: x in ( dom ( Im (f (#) g)));

 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;

 end;

 hence thesis by A16, A17, A13, A14, A3, A8, A5, A4, FUNCT_1: 2;

 end;

 theorem :: MESFUN7C:33

 (( dom f) /\ ( dom g)) = E & f is E -measurable & g is E -measurable implies (f (#) g) is E -measurable

 proof

 assume that

 A1: (( dom f) /\ ( dom g)) = E and

 A2: f is E -measurable and

 A3: g is E -measurable;



 A4: ( dom ( Im g)) = ( dom g) by COMSEQ_3:def 4;



 A5: ( Im f) is E -measurable 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 E -measurable by A3, MESFUN6C:def 1;

 then

 A9: (( Im f) (#) ( Im g)) is E -measurable 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 E -measurable by A3, MESFUN6C:def 1;

 then

 A13: (( Im f) (#) ( Re g)) is E -measurable by A1, A5, A6, A11, Th31;



 A14: ( Re f) is E -measurable by A2, MESFUN6C:def 1;

 then (( Re f) (#) ( Im g)) is E -measurable by A1, A8, A10, A4, Th31;

 then ((( Im f) (#) ( Re g)) + (( Re f) (#) ( Im g))) is E -measurable by A13, MESFUNC6: 26;

 then

 A15: ( Im (f (#) g)) is E -measurable by Th32;

 (( Re f) (#) ( Re g)) is E -measurable by A1, A14, A12, A10, A11, Th31;

 then ((( Re f) (#) ( Re g)) - (( Im f) (#) ( Im g))) is E -measurable by A9, A7, MESFUNC6: 29;

 then ( Re (f (#) g)) is E -measurable by Th32;

 hence thesis by A15, MESFUN6C:def 1;

 end;

 theorem :: MESFUN7C:34



 Th34: for f,g be PartFunc of X, REAL st (ex E be Element of S st E = ( dom f) & E = ( dom g) & f is E -measurable & g is E -measurable) & f is nonnegative & g is nonnegative & (for x be Element of X st x in ( dom g) holds (g . x) <= (f . x)) holds ( Integral (M,g)) <= ( Integral (M,f))

 proof

 let f,g be PartFunc of X, REAL ;

 assume that

 A1: ex A be Element of S st A = ( dom f) & A = ( dom g) & f is A -measurable & g is A -measurable and

 A2: f is nonnegative & g is nonnegative and

 A3: for x be Element of X st x in ( dom g) holds (g . x) <= (f . x);



 A4: ( Integral (M,g)) = ( integral+ (M,( R_EAL g))) & ( Integral (M,f)) = ( integral+ (M,( R_EAL f))) by A1, A2, MESFUNC6: 82;

 consider A be Element of S such that

 A5: A = ( dom f) & A = ( dom g) and

 A6: f is A -measurable & g is A -measurable by A1;

 ( R_EAL f) is A -measurable & ( R_EAL g) is A -measurable by A6, MESFUNC6:def 1;

 hence thesis by A2, A3, A5, A4, MESFUNC5: 85;

 end;

 theorem :: MESFUN7C:35



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

 proof

 let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, COMPLEX ;

 assume

 A1: 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 be Element of S such that

 A2: A1 = ( dom ( R_EAL ( Re f))) and

 A3: ( R_EAL ( Re f)) is A1 -measurable;



 A4: ( Re f) is A1 -measurable 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 be Element of S such that

 A5: A2 = ( dom ( R_EAL ( Im f))) and

 A6: ( R_EAL ( Im f)) is A2 -measurable;



 A7: A1 = ( dom f) by A2, COMSEQ_3:def 3;

 A2 = ( dom f) by A5, COMSEQ_3:def 4;

 then ( Im f) is A1 -measurable by A6, A7, MESFUNC6:def 1;

 then

 A8: f is A1 -measurable by A4, MESFUN6C:def 1;

 hence ex A be Element of S st A = ( dom f) & f is A -measurable by A7;

 thus thesis by A1, A7, A8, MESFUN6C: 31;

 end;

 theorem :: MESFUN7C:36

 f is_integrable_on M implies ex F be sequence of S st (for n be Nat holds (F . n) = (( dom f) /\ ( great_eq_dom ( |.f.|,(1 / (n + 1)))))) & (( dom f) \ ( eq_dom ( |.f.|, 0 ))) = ( union ( rng F)) & for n be Nat holds (F . n) in S & (M . (F . n)) < +infty

 proof

 assume

 A1: f is_integrable_on M;

 then

 consider E be Element of S such that

 A2: E = ( dom f) and

 A3: f is E -measurable by Th35;

 defpred P[ 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

 let x be object;

 reconsider y = ( |.f.| . x) as Real;

 assume

 A5: x in (E \ ( eq_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;

 end;

 then

 A8: (E \ ( eq_dom ( |.f.|, 0 ))) c= (E /\ ( great_dom ( |.f.|, 0 )));

 now

 let x be object;

 assume

 A9: x in (E /\ ( great_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;

 end;

 then

 A11: (E /\ ( great_dom ( |.f.|, 0 ))) c= (E \ ( eq_dom ( |.f.|, 0 )));



 A12: |.f.| is E -measurable by A2, A3, MESFUN6C: 30;



 A13: for n be Element of NAT holds ex Z be Element of S st P[n, Z]

 proof

 let n be Element of NAT ;

 take (E /\ ( great_eq_dom ( |.f.|,(1 / (n + 1)))));

 thus thesis by A12, A4, MESFUNC6: 13;

 end;

 consider F be sequence of S such that

 A14: for n be Element of NAT holds P[n, (F . n)] from FUNCT_2:sch 3( A13);



 A15: for n be 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;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

 set z = (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 be PartFunc of X, REAL such that

 A18: nf is_simple_func_in S and

 A19: ( dom nf) = En and

 A20: for x be object st x in En holds (nf . x) = (1 / (n + 1)) by MESFUNC6: 75;



 A21: ( dom h) = 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 be Element of X st x in ( dom nf) holds (nf . x) <= (h . x)

 proof

 let x be Element of X;

 assume

 A24: x in ( dom nf);

 then (h . x) = ( |.f.| . x) by A19, FUNCT_1: 49;

 then (1 / (n + 1)) <= (h . x) by A22, A19, A24, MESFUNC1:def 14;

 hence thesis by A19, A20, A24;

 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 En -measurable by A12, A17, MESFUNC6: 16, XBOOLE_1: 17;

 then

 A26: h is En -measurable by A25, MESFUNC6: 76;



 A27: h is nonnegative by Lm1, MESFUNC6: 55;

 for x be object 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;

 then

 A29: ( Integral (M,h)) <= ( Integral (M, |.f.|)) by A12, A4, A17, MESFUNC6: 87, XBOOLE_1: 17;

 nf is En -measurable by A18, MESFUNC6: 50;

 then ( Integral (M,nf)) <= ( Integral (M,h)) by A21, A26, A27, A19, A28, A23, Th34;

 then

 A30: ( Integral (M,nf)) <= ( Integral (M, |.f.|)) by A29, XXREAL_0: 2;



 A31: ((z * (M . En)) / z) = (M . En) & ( +infty / z) = +infty by XXREAL_3: 83, XXREAL_3: 88;

 ( Integral (M,nf)) = ((1 / (n + 1)) * (M . En)) by A19, A20, MESFUNC6: 97;

 then ((1 / (n + 1)) * (M . En)) < +infty by A16, A30, XXREAL_0: 2;

 hence thesis by A31, XXREAL_3: 80;

 end;

 take F;



 A32: for n be Nat holds (F . n) = (E /\ ( great_eq_dom ( |.f.|,(1 / (n + 1)))))

 proof

 let n be Nat;

 n in NAT by ORDINAL1:def 12;

 hence thesis by A14;

 end;

 then for n be 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 thesis by A2, A32, A11, A8, A15;

 end;

 reserve x,A for set;

 theorem :: MESFUN7C:37



 Th37: ( |.f.| | A) = |.(f | A).|

 proof

 ( 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

 let x be Element of X;

 assume

 A4: x in ( dom ( |.f.| | A));

 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;

 end;

 hence thesis by A1, A3, PARTFUN1: 5;

 end;

 theorem :: MESFUN7C:38



 Th38: ( dom ( |.f.| + |.g.|)) = (( dom f) /\ ( dom g)) & ( dom |.(f + g).|) c= ( dom |.f.|)

 proof

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

 ( 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 thesis by VALUED_1:def 11;

 end;

 theorem :: MESFUN7C:39



 Th39: (( |.f.| | ( dom |.(f + g).|)) + ( |.g.| | ( dom |.(f + g).|))) = (( |.f.| + |.g.|) | ( dom |.(f + g).|))

 proof



 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

 let x be Element of X;

 assume

 A13: x in ( dom (( |.f.| + |.g.|) | ( dom |.(f + g).|)));



 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;

 end;

 hence thesis by A11, A7, PARTFUN1: 5, RELAT_1: 62;

 end;

 theorem :: MESFUN7C:40



 Th40: x in ( dom |.(f + g).|) implies ( |.(f + g).| . x) <= (( |.f.| + |.g.|) . x)

 proof



 A1: |.((f . x) + (g . x)).| <= ( |.(f . x).| + |.(g . x).|) by COMPLEX1: 56;

 assume

 A2: x in ( dom |.(f + g).|);

 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 thesis by A2, A3, VALUED_1:def 11;

 end;

 theorem :: MESFUN7C:41



 Th41: for f,g be PartFunc of X, REAL st (for x be set st x in ( dom f) holds (f . x) <= (g . x)) holds (g - f) is nonnegative

 proof

 let f,g be PartFunc of X, REAL ;

 assume

 A1: for x be set st x in ( dom f) holds (f . x) <= (g . x);

 now

 let x be object;

 assume

 A2: x in ( dom (g - f));

 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;

 end;

 hence thesis by MESFUNC6: 52;

 end;

 theorem :: MESFUN7C:42

 f is_integrable_on M & g is_integrable_on M implies ex E be Element of S st E = ( dom (f + g)) & ( Integral (M,( |.(f + g).| | E))) <= (( Integral (M,( |.f.| | E))) + ( Integral (M,( |.g.| | E))))

 proof

 assume that

 A1: f is_integrable_on M and

 A2: g is_integrable_on M;

 |.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 be Element of S such that

 A4: B2 = ( dom ( R_EAL ( Im g))) & ( R_EAL ( Im g)) is B2 -measurable;

 ( 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 be Element of S such that

 A5: A2 = ( dom ( R_EAL ( Im f))) & ( R_EAL ( Im f)) is A2 -measurable;

 ( 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 be Element of S such that

 A6: B1 = ( dom ( R_EAL ( Re g))) and

 A7: ( R_EAL ( Re g)) is B1 -measurable;



 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 be 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 be Element of S such that

 A11: A1 = ( dom ( R_EAL ( Re f))) and

 A12: ( R_EAL ( Re f)) is A1 -measurable;



 A13: A1 = ( dom f) by A11, COMSEQ_3:def 3;

 reconsider A = (A1 /\ B1) as Element of S;

 ( Re f) is A1 -measurable by A12, MESFUNC6:def 1;

 then

 A14: ( Re f) is A -measurable 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 B1 -measurable by A7, MESFUNC6:def 1;

 then

 A17: ( Re g) is A -measurable by MESFUNC6: 16, XBOOLE_1: 17;

 B2 = ( dom g) & ( Im g) is B2 -measurable by A4, COMSEQ_3:def 4, MESFUNC6:def 1;

 then ( Im g) is A -measurable by A8, MESFUNC6: 16, XBOOLE_1: 17;

 then

 A18: g is A -measurable by A17, MESFUN6C:def 1;

 then

 A19: |.g.| is A -measurable by A8, MESFUN6C: 30, XBOOLE_1: 17;

 A2 = ( dom f) & ( Im f) is A2 -measurable by A5, COMSEQ_3:def 4, MESFUNC6:def 1;

 then ( Im f) is A -measurable by A13, MESFUNC6: 16, XBOOLE_1: 17;

 then

 A20: f is A -measurable by A14, MESFUN6C:def 1;

 then |.f.| is A -measurable by A13, MESFUN6C: 30, XBOOLE_1: 17;

 then

 A21: ( |.f.| + |.g.|) is A -measurable 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 A -measurable by A13, A8, A20, A18, A15, MESFUN6C: 11, MESFUN6C: 30;

 then

 consider E be 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;

 thus E = ( dom (f + g)) by A13, A8, A15, A24, A22, A23, A16, A26, XBOOLE_1: 19, XBOOLE_1: 28;

 (F | E) is_integrable_on M & (G | E) is_integrable_on M by A1, A2, Th35, MESFUNC6: 91;

 then

 consider E1 be 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;

 hence thesis by A16, A25, A26, A27, A30, Th39;

 end;

 begin

 definition

 let X be non empty set;

 let S be SigmaField of X;

 let f be PartFunc of X, COMPLEX ;

 :: MESFUN7C:def13

 pred f is_simple_func_in S means ex F be Finite_Sep_Sequence of S st ( dom f) = ( union ( rng F)) & for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y);

 end

 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 ;

 :: MESFUN7C:def14

 pred F,a are_Re-presentation_of f means ( dom f) = ( union ( rng F)) & ( dom F) = ( dom a) & for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (f . x) = (a . n);

 end

 definition

 let X, S, f;

 let F be Finite_Sep_Sequence of S;

 let a be FinSequence of COMPLEX ;

 :: MESFUN7C:def15

 pred F,a are_Re-presentation_of f means ( dom f) = ( union ( rng F)) & ( dom F) = ( dom a) & for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (f . x) = (a . n);

 end

 theorem :: MESFUN7C:43

 f is_simple_func_in S iff ( Re f) is_simple_func_in S & ( Im f) is_simple_func_in S

 proof

 hereby

 assume f is_simple_func_in S;

 then

 consider F be Finite_Sep_Sequence of S such that

 A1: ( dom f) = ( union ( rng F)) and

 A2: for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y);



 A3: ( dom ( Im f)) = ( union ( rng F)) by A1, COMSEQ_3:def 4;



 A4: for n be Nat, x,y be 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, x,y be Element of X;

 assume that

 A5: n in ( dom F) and

 A6: x in (F . n) & y in (F . n);

 (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 thesis by A2, A5, A6;

 end;



 A7: ( dom ( Re f)) = ( union ( rng F)) by A1, COMSEQ_3:def 3;

 for n be Nat, x,y be 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, x,y be Element of X;

 assume that

 A8: n in ( dom F) and

 A9: x in (F . n) & y in (F . n);

 (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 thesis by A2, A8, A9;

 end;

 hence ( Re f) is_simple_func_in S & ( Im f) is_simple_func_in S by A7, A3, A4, MESFUNC6:def 2;

 end;

 assume that

 A10: ( Re f) is_simple_func_in S and

 A11: ( Im f) is_simple_func_in S;

 consider F be Finite_Sep_Sequence of S such that

 A12: ( dom ( Re f)) = ( union ( rng F)) and

 A13: for n be Nat, x,y be 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 be Finite_Sep_Sequence of S such that

 A15: ( dom ( Im f)) = ( union ( rng G)) and

 A16: for n be Nat, x,y be 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 FG1( Nat) = ((F . ((($1 -' 1) div lb) + 1)) /\ (G . ((($1 -' 1) mod lb) + 1)));

 consider FG be FinSequence such that

 A17: ( len FG) = (la * lb) and

 A18: for k be Nat st k in ( dom FG) holds (FG . k) = FG1(k) from FINSEQ_1:sch 2;



 A19: ( dom FG) = ( Seg (la * lb)) by A17, FINSEQ_1:def 3;

 now

 let k be Nat;



 A20: lb divides (la * lb) by NAT_D:def 3;

 set j = (((k -' 1) mod lb) + 1);

 set i = (((k -' 1) div lb) + 1);

 assume

 A21: k in ( dom FG);

 then

 A22: 1 <= k by FINSEQ_3: 25;

 then

 A23: lb > 0 by A17, A21, FINSEQ_3: 25;



 A24: k <= (la * lb) by A17, A21, FINSEQ_3: 25;

 then (k -' 1) <= ((la * lb) -' 1) by NAT_D: 42;

 then

 A25: ((k -' 1) div lb) <= (((la * lb) -' 1) div lb) by NAT_2: 24;



 A26: 1 <= (la * lb) by A22, A24, XXREAL_0: 2;

 1 <= lb by A23, NAT_1: 14;

 then (((la * lb) -' 1) div lb) = (((la * lb) div lb) - 1) by A26, A20, NAT_2: 15;

 then i <= ((la * lb) div lb) by A25, XREAL_1: 19;

 then i >= 1 & i <= la by A23, NAT_1: 14, NAT_D: 18;

 then i in ( dom F) by FINSEQ_3: 25;

 then

 A27: (F . i) in ( rng F) by FUNCT_1: 3;

 ((k -' 1) mod lb) < lb by A23, NAT_D: 1;

 then j >= 1 & j <= lb by NAT_1: 13, NAT_1: 14;

 then j in ( dom G) by FINSEQ_3: 25;

 then (G . j) in ( rng G) by FUNCT_1: 3;

 then ((F . i) /\ (G . j)) in S by A27, MEASURE1: 34;

 hence (FG . k) in S by A18, A21;

 end;

 then

 reconsider FG as FinSequence of S by FINSEQ_2: 12;

 for k,l be Nat st k in ( dom FG) & l in ( dom FG) & k <> l holds (FG . k) misses (FG . l)

 proof

 let k,l be Nat;

 assume that

 A28: k in ( dom FG) and

 A29: l in ( dom FG) and

 A30: k <> l;

 set m = (((l -' 1) mod lb) + 1);

 set n = (((l -' 1) div lb) + 1);



 A31: 1 <= k by A28, FINSEQ_3: 25;

 then

 A32: lb > 0 by A17, A28, FINSEQ_3: 25;

 then

 A33: ((l -' 1) + 1) = ((((n - 1) * lb) + (m - 1)) + 1) by NAT_D: 2;



 A34: k <= (la * lb) by A17, A28, FINSEQ_3: 25;

 then

 A35: lb divides (la * lb) & 1 <= (la * lb) by A31, NAT_1: 14, NAT_D:def 3;

 1 <= lb by A32, NAT_1: 14;

 then

 A36: (((la * lb) -' 1) div lb) = (((la * lb) div lb) - 1) by A35, NAT_2: 15;

 set j = (((k -' 1) mod lb) + 1);

 set i = (((k -' 1) div lb) + 1);

 (FG . k) = ((F . i) /\ (G . j)) by A18, A28;



 then

 A37: ((FG . k) /\ (FG . l)) = (((F . i) /\ (G . j)) /\ ((F . n) /\ (G . m))) by A18, A29

 .= ((F . i) /\ ((G . j) /\ ((F . n) /\ (G . m)))) by XBOOLE_1: 16

 .= ((F . i) /\ ((F . n) /\ ((G . j) /\ (G . m)))) by XBOOLE_1: 16

 .= (((F . i) /\ (F . n)) /\ ((G . j) /\ (G . m))) by XBOOLE_1: 16;

 l <= (la * lb) by A17, A29, FINSEQ_3: 25;

 then (l -' 1) <= ((la * lb) -' 1) by NAT_D: 42;

 then ((l -' 1) div lb) <= (((la * lb) div lb) - 1) by A36, NAT_2: 24;

 then (((l -' 1) div lb) + 1) <= ((la * lb) div lb) by XREAL_1: 19;

 then n >= 1 & n <= la by A32, NAT_1: 14, NAT_D: 18;

 then n in ( Seg la);

 then

 A38: n in ( dom F) by FINSEQ_1:def 3;

 1 <= l by A29, FINSEQ_3: 25;

 then

 A39: ((l - 1) + 1) = (((n - 1) * lb) + m) by A33, XREAL_1: 233;

 ((l -' 1) mod lb) < lb by A32, NAT_D: 1;

 then m >= 1 & m <= lb by NAT_1: 13, NAT_1: 14;

 then m in ( Seg lb);

 then

 A40: m in ( dom G) by FINSEQ_1:def 3;

 (k -' 1) <= ((la * lb) -' 1) by A34, NAT_D: 42;

 then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A36, NAT_2: 24;

 then (((k -' 1) div lb) + 1) <= ((la * lb) div lb) by XREAL_1: 19;

 then i >= 1 & i <= la by A32, NAT_1: 11, NAT_D: 18;

 then i in ( Seg la);

 then

 A41: i in ( dom F) by FINSEQ_1:def 3;

 ((k -' 1) + 1) = ((((i - 1) * lb) + (j - 1)) + 1) by A32, NAT_D: 2;

 then

 A42: ((k - 1) + 1) = (((i - 1) * lb) + j) by A31, XREAL_1: 233;

 ((k -' 1) mod lb) < lb by A32, NAT_D: 1;

 then j >= 1 & j <= lb by NAT_1: 11, NAT_1: 13;

 then j in ( Seg lb);

 then

 A43: j in ( dom G) by FINSEQ_1:def 3;

 per cases by A30, A42, A39;

 suppose i <> n;

 then (F . i) misses (F . n) by A41, A38, MESFUNC3: 4;

 then ((FG . k) /\ (FG . l)) = ( {} /\ ((G . j) /\ (G . m))) by A37;

 hence thesis;

 end;

 suppose j <> m;

 then (G . j) misses (G . m) by A43, A40, MESFUNC3: 4;

 then ((FG . k) /\ (FG . l)) = (((F . i) /\ (F . n)) /\ {} ) by A37;

 hence thesis;

 end;

 end;

 then

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

 proof

 let z be object;

 assume

 A46: z in ( dom f);

 then

 consider Y be set such that

 A47: z in Y and

 A48: Y in ( rng F) by A14, TARSKI:def 4;

 consider Z be set such that

 A49: z in Z and

 A50: Z in ( rng G) by A44, A46, TARSKI:def 4;

 consider j be Nat such that

 A51: j in ( dom G) and

 A52: Z = (G . j) by A50, FINSEQ_2: 10;

 consider i be 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 be Nat such that

 A55: i = (1 + i9 qua Complex) by NAT_1: 10;

 set k = (((i - 1) * lb) + j);

 reconsider k as Nat by A55;

 i <= la by A53, FINSEQ_3: 25;

 then (i - 1) <= (la - 1) by XREAL_1: 9;

 then ((i - 1) * lb) <= ((la - 1) * lb) by XREAL_1: 64;

 then

 A56: k <= (((la - 1) * lb) + j) by XREAL_1: 6;



 A57: j <= lb by A51, FINSEQ_3: 25;

 then (((la - 1) * lb) + j) <= (((la - 1) * lb) + lb) by XREAL_1: 6;

 then

 A58: k <= (la * lb) by A56, XXREAL_0: 2;



 A59: 1 <= j by A51, FINSEQ_3: 25;

 then

 consider j9 be Nat such that

 A60: j = (1 + j9 qua Complex) by NAT_1: 10;



 A61: j9 < lb 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 * lb) + j9) by A55, A60;

 then

 A64: i = (((k -' 1) div lb) + 1) by A55, A61, NAT_D:def 1;



 A65: k >= 1 by A59, A62, XXREAL_0: 2;

 then

 A66: k in ( Seg (la * lb)) by A58;



 A67: j = (((k -' 1) mod lb) + 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 thesis by A68, TARSKI:def 4;

 end;

 let z be object;

 assume z in ( union ( rng FG));

 then

 consider Y be set such that

 A69: z in Y and

 A70: Y in ( rng FG) by TARSKI:def 4;

 consider k be 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: lb > 0 by A17, A71, FINSEQ_3: 25;

 then

 A75: 1 <= lb by NAT_1: 14;



 A76: k <= (la * lb) by A17, A71, FINSEQ_3: 25;

 then lb divides (la * lb) & 1 <= (la * lb) by A73, NAT_1: 14, NAT_D:def 3;

 then

 A77: (((la * lb) -' 1) div lb) = (((la * lb) div lb) - 1) by A75, NAT_2: 15;

 set j = (((k -' 1) mod lb) + 1);

 set i = (((k -' 1) div lb) + 1);

 (k -' 1) <= ((la * lb) -' 1) by A76, NAT_D: 42;

 then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A77, NAT_2: 24;

 then

 A78: i >= 1 & i <= ((la * lb) div lb) by NAT_1: 14, XREAL_1: 19;

 ((la * lb) div lb) = la by A74, NAT_D: 18;

 then i in ( dom F) by A78, FINSEQ_3: 25;

 then

 A79: (F . i) in ( rng F) by FUNCT_1:def 3;

 (FG . k) = ((F . i) /\ (G . j)) by A18, A71;

 then z in (F . i) by A69, A72, XBOOLE_0:def 4;

 hence thesis by A14, A79, TARSKI:def 4;

 end;

 for k be Nat, x,y be 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;

 let x,y be Element of X;

 set i = (((k -' 1) div lb) + 1);

 set j = (((k -' 1) mod lb) + 1);

 assume that

 A80: k in ( dom FG) and

 A81: x in (FG . k) & y in (FG . k);



 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: lb > 0 by A17, A80, FINSEQ_3: 25;

 then ((k -' 1) mod lb) < lb by NAT_D: 1;

 then j >= 1 & j <= lb by NAT_1: 13, NAT_1: 14;

 then

 A86: j 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 <= (la * lb) by A17, A80, FINSEQ_3: 25;

 then

 A89: (k -' 1) <= ((la * lb) -' 1) by NAT_D: 42;



 A90: (FG . k) = ((F . (((k -' 1) div lb) + 1)) /\ (G . (((k -' 1) mod lb) + 1))) by A18, A80;

 then x in (G . j) & y in (G . j) by A81, XBOOLE_0:def 4;

 then

 A91: ( Im (f . x)) = ( Im (f . y)) by A16, A86, A83;



 A92: lb divides (la * lb) & 1 <= (la * lb) by A84, A88, NAT_1: 14, NAT_D:def 3;

 1 <= lb by A85, NAT_1: 14;

 then (((la * lb) -' 1) div lb) = (((la * lb) div lb) - 1) by A92, NAT_2: 15;

 then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A89, NAT_2: 24;

 then i <= ((la * lb) div lb) by XREAL_1: 19;

 then i >= 1 & i <= la by A85, NAT_1: 14, NAT_D: 18;

 then

 A93: i in ( dom F) by FINSEQ_3: 25;

 x in (F . i) & y in (F . i) by A81, A90, XBOOLE_0:def 4;

 then ( Re (f . x)) = ( Re (f . y)) by A13, A93, A87;

 hence thesis by A91;

 end;

 hence thesis by A45;

 end;

 theorem :: MESFUN7C:44



 Th44: f is_simple_func_in S implies ex F be Finite_Sep_Sequence of S, a be FinSequence of COMPLEX st ( dom f) = ( union ( rng F)) & ( dom F) = ( dom a) & for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (f . x) = (a . n)

 proof

 assume f is_simple_func_in S;

 then

 consider F be Finite_Sep_Sequence of S such that

 A1: ( dom f) = ( union ( rng F)) and

 A2: for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y);

 defpred P[ set, set] means for x be set st x in (F . $1) holds $2 = (f . x);



 A3: for k be Nat st k in ( Seg ( len F)) holds ex y be Element of COMPLEX st P[k, y]

 proof

 let k be Nat;

 assume k in ( Seg ( len F));

 then

 A4: k in ( dom F) by FINSEQ_1:def 3;

 then

 A5: (F . k) in ( rng F) by FUNCT_1: 3;

 per cases ;

 suppose

 A6: (F . k) = {} ;

 0 in REAL by XREAL_0:def 1;

 then

 reconsider y = 0 as Element of COMPLEX by NUMBERS: 11;

 take y;

 thus thesis by A6;

 end;

 suppose (F . k) <> {} ;

 then

 consider x1 be object 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;

 hereby

 let x be set;



 A8: ( rng F) c= ( bool X) by XBOOLE_1: 1;

 assume x in (F . k);

 hence y = (f . x) by A2, A4, A5, A7, A8;

 end;

 end;

 end;

 consider a be FinSequence of COMPLEX such that

 A9: ( dom a) = ( Seg ( len F)) & for k be Nat st k in ( Seg ( len F)) holds P[k, (a . k)] from FINSEQ_1:sch 5( A3);

 take F, a;

 now

 let n be Nat;

 assume n in ( dom F);

 then n in ( Seg ( len F)) by FINSEQ_1:def 3;

 hence for x be set st x in (F . n) holds (a . n) = (f . x) by A9;

 end;

 hence thesis by A1, A9, FINSEQ_1:def 3;

 end;

 theorem :: MESFUN7C:45



 Th45: f is_simple_func_in S iff ex F be Finite_Sep_Sequence of S, a be FinSequence of COMPLEX st (F,a) are_Re-presentation_of f

 proof

 hereby

 assume f is_simple_func_in S;

 then

 consider F be Finite_Sep_Sequence of S, a be FinSequence of COMPLEX such that

 A1: ( dom f) = ( union ( rng F)) & ( dom F) = ( dom a) & for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (f . x) = (a . n) by Th44;

 take F, a;

 thus (F,a) are_Re-presentation_of f by A1;

 end;

 given F be Finite_Sep_Sequence of S, a be FinSequence of COMPLEX such that

 A2: (F,a) are_Re-presentation_of f;



 A3: for n be Nat, x,y be 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, x,y be Element of X;

 assume that

 A4: n in ( dom F) and

 A5: x in (F . n) and

 A6: y in (F . n);

 (f . x) = (a . n) by A2, A4, A5;

 hence thesis by A2, A4, A6;

 end;

 ( dom f) = ( union ( rng F)) by A2;

 hence thesis by A3;

 end;

 reserve c for FinSequence of COMPLEX ;

 theorem :: MESFUN7C:46



 Th46: for n be Nat st n in ( dom ( Re c)) holds (( Re c) . n) = ( Re (c . n))

 proof

 let n be Nat;



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

 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)) * )) by COMPLEX1: 13;

 hence thesis by A6;

 end;

 theorem :: MESFUN7C:47



 Th47: for n be Nat st n in ( dom ( Im c)) holds (( Im c) . n) = ( Im (c . n))

 proof

 let n be Nat;

 assume

 A1: n in ( dom ( Im c));

 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) * )) * (c *' )) . n) = (( - ((1 / 2) * )) * ((c *' ) . n)) by COMPLSP2: 16

 .= (( - ((1 / 2) * )) * ((c . n) *' )) by A2, A3, COMPLSP2:def 1;

 ( len (( - ((1 / 2) * )) * c)) = ( len c) & ( len (( - ((1 / 2) * )) * (c *' ))) = ( len (c *' )) by COMPLSP2: 3;

 then

 A5: ( 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: 43, ORDINAL1:def 12;

 then (( Im c) . n) = (((( - ((1 / 2) * )) * c) . n) - ((( - ((1 / 2) * )) * (c *' )) . n)) by A5, COMPLSP2: 25;

 then

 A6: (( Im c) . n) = ((( - ((1 / 2) * )) * (c . n)) - (( - ((1 / 2) * )) * ((c . n) *' ))) by A4, COMPLSP2: 16;

 ((c . n) - ((c . n) *' )) = ((( Re (c . n)) + (( Im (c . n)) * )) - (( Re (c . n)) - (( Im (c . n)) * ))) by COMPLEX1: 13;

 hence thesis by A6;

 end;

 theorem :: MESFUN7C:48



 Th48: for F be Finite_Sep_Sequence of S, a be 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 F be Finite_Sep_Sequence of S, a be FinSequence of COMPLEX ;

 hereby

 assume

 A1: (F,a) are_Re-presentation_of f;

 ( len ( Im a)) = ( len a) by COMPLSP2: 48;

 then ( dom ( Im a)) = ( Seg ( len a)) by FINSEQ_1:def 3;

 then ( dom ( Im a)) = ( dom a) by FINSEQ_1:def 3;

 then

 A2: ( dom F) = ( dom ( Im a)) by A1;

 ( dom ( Im f)) = ( dom f) by COMSEQ_3:def 4;

 then

 A3: ( dom ( Im f)) = ( union ( rng F)) by A1;



 A4: for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (( Im f) . x) = (( Im a) . n)

 proof

 let n be Nat;

 assume

 A5: n in ( dom F);

 let x be set;

 assume

 A6: x in (F . n);

 (F . n) c= ( union ( rng F)) by A5, MESFUNC3: 7;

 then x in ( dom ( Im f)) by A3, A6;

 then

 A7: (( Im f) . x) = ( Im (f . x)) by COMSEQ_3:def 4;

 ( Im (f . x)) = ( Im (a . n)) by A1, A5, A6;

 hence thesis by A2, A5, A7, Th47;

 end;

 ( len ( Re a)) = ( len a) by COMPLSP2: 48;

 then ( dom ( Re a)) = ( Seg ( len a)) by FINSEQ_1:def 3;

 then ( dom ( Re a)) = ( dom a) by FINSEQ_1:def 3;

 then

 A8: ( dom F) = ( dom ( Re a)) by A1;

 ( dom ( Re f)) = ( dom f) by COMSEQ_3:def 3;

 then

 A9: ( dom ( Re f)) = ( union ( rng F)) by A1;

 for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (( Re f) . x) = (( Re a) . n)

 proof

 let n be Nat;

 assume

 A10: n in ( dom F);

 let x be set;

 assume

 A11: x in (F . n);

 (F . n) c= ( union ( rng F)) by A10, MESFUNC3: 7;

 then x in ( dom ( Re f)) by A9, A11;

 then

 A12: (( Re f) . x) = ( Re (f . x)) by COMSEQ_3:def 3;

 ( Re (f . x)) = ( Re (a . n)) by A1, A10, A11;

 hence thesis by A8, A10, A12, Th46;

 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;

 end;

 assume that

 A13: (F,( Re a)) are_Re-presentation_of ( Re f) and

 A14: (F,( Im a)) are_Re-presentation_of ( Im f);



 A15: ( dom F) = ( dom ( Re a)) by A13;



 A16: ( dom ( Re f)) = ( union ( rng F)) by A13;

 then

 A17: ( dom f) = ( union ( rng F)) by COMSEQ_3:def 3;



 A18: ( dom F) = ( dom ( Im a)) by A14;



 A19: ( dom ( Im f)) = ( union ( rng F)) by A14;



 A20: for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (f . x) = (a . n)

 proof

 let n be Nat;

 assume

 A21: n in ( dom F);

 let x be set;

 assume

 A22: x in (F . n);



 A23: (F . n) c= ( union ( rng F)) by A21, MESFUNC3: 7;

 then x in ( dom ( Im f)) by A19, A22;

 then

 A24: (( Im f) . x) = ( Im (f . x)) by COMSEQ_3:def 4;

 x in ( dom ( Re f)) by A16, A22, A23;

 then

 A25: (( Re f) . x) = ( Re (f . x)) by COMSEQ_3:def 3;

 (( Im f) . x) = (( Im a) . n) by A14, A21, A22;

 then

 A26: ( Im (f . x)) = ( Im (a . n)) by A18, A21, A24, Th47;

 (( Re f) . x) = (( Re a) . n) by A13, A21, A22;

 then ( Re (f . x)) = ( Re (a . n)) by A15, A21, A25, Th46;

 hence thesis by A26;

 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 thesis by A17, A20;

 end;

 theorem :: MESFUN7C:49

 f is_simple_func_in S iff ex F be Finite_Sep_Sequence of S, c be FinSequence of COMPLEX st ( dom f) = ( union ( rng F)) & ( dom F) = ( dom c) & (for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (( Re f) . x) = (( Re c) . n)) & for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (( Im f) . x) = (( Im c) . n)

 proof

 hereby

 assume f is_simple_func_in S;

 then

 consider F be Finite_Sep_Sequence of S, c be 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 be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (( Im f) . x) = (( Im c) . n);

 (F,( Re c)) are_Re-presentation_of ( Re f) by A1, Th48;

 then

 A3: for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (( Re f) . x) = (( Re c) . n);

 ( dom f) = ( union ( rng F)) & ( dom F) = ( dom c) by A1;

 hence ex F be Finite_Sep_Sequence of S, c be FinSequence of COMPLEX st ( dom f) = ( union ( rng F)) & ( dom F) = ( dom c) & (for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (( Re f) . x) = (( Re c) . n)) & for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (( Im f) . x) = (( Im c) . n) by A3, A2;

 end;

 given F be Finite_Sep_Sequence of S, c be FinSequence of COMPLEX such that

 A4: ( dom f) = ( union ( rng F)) and

 A5: ( dom F) = ( dom c) and

 A6: for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (( Re f) . x) = (( Re c) . n) and

 A7: for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (( Im f) . x) = (( Im c) . n);



 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 be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (f . x) = (c . n)

 proof

 let n be Nat;

 assume

 A12: n in ( dom F);

 let x be set;

 assume

 A13: x in (F . 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 thesis by A17;

 end;

 then (F,c) are_Re-presentation_of f by A4, A5;

 hence thesis by Th45;

 end;