:: Integral of Complex-Valued Measurable Function
::  by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received July 30, 2008
:: Copyright (c) 2008-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, MEASURE6, ARYTM_3, ARYTM_1, RELAT_1, REAL_1, XBOOLE_0,
      PARTFUN1, COMPLEX1, SUBSET_1, FUNCT_1, PROB_1, MEASURE1, XCMPLX_0,
      MESFUNC1, VALUED_1, CARD_1, TARSKI, INTEGRA5, MESFUNC5, XXREAL_0,
      RFUNCT_3, SUPINF_2, POWER, SQUARE_1, PREPOWER;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XXREAL_3,
      XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, VALUED_1, SUPINF_2, PREPOWER, POWER, SQUARE_1, MEASURE6,
      MEASURE1, EXTREAL1, COMSEQ_3, VALUED_0, MESFUNC1, MESFUNC2, PROB_1,
      MESFUNC5, MESFUNC6;
 constructors REAL_1, PREPOWER, POWER, SQUARE_1, COMPLEX1, MEASURE6, EXTREAL1,
      MESFUNC1, MESFUNC2, MESFUNC5, MESFUNC6, SUPINF_1, RELSET_1, ABIAN,
      BINOP_2, VALUED_0, COMSEQ_3;
 registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
      MEASURE1, VALUED_0, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, SQUARE_1,
      ORDINAL1, XXREAL_3;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions SUPINF_2;
 equalities MESFUNC5, VALUED_1, MESFUNC6, COMPLEX1, XCMPLX_0;
 expansions MESFUNC5, MESFUNC6;
 theorems TARSKI, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, MESFUNC1, XBOOLE_0,
      XBOOLE_1, XCMPLX_1, HOLDER_1, PREPOWER, MESFUNC2, XREAL_1, MESFUNC5,
      XXREAL_0, VALUED_1, MESFUNC6, SUBSET_1, COMPLEX1, XREAL_0, RELAT_1,
      POWER, SQUARE_1, RELSET_1, FINSUB_1, COMSEQ_3, XCMPLX_0;
 schemes SEQ_1;

begin :: Definitions for Complex-valued Functions

theorem
  for a,b be Real holds a + b = a+b & - a =
  -a & a - b = a-b & a * b = a*b;

begin :: The Measurability of Complex-valued Functions

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,
  c for Complex,
  E,A,B for Element of S;

definition
  let X be non empty set;
  let S be SigmaField of X;
  let E be Element of S;
  let f be PartFunc of X,COMPLEX;
  attr f is E-measurable means
  Re f is E-measurable & Im f is E-measurable;
end;

theorem Th2:
  r(#)(Re f) = Re(r(#)f) & r(#)(Im f) = Im(r(#)f)
proof
A1: dom(r(#)(Re f)) = dom Re f by VALUED_1:def 5;
A3: Im r = 0 by COMPLEX1:def 2;
A4: dom Re f = dom f by COMSEQ_3:def 3;
A5: Re r = r by COMPLEX1:def 1;
A6: dom(r(#)f) = dom f by VALUED_1:def 5;
A7: dom Re(r(#)f) = dom(r(#)f) by COMSEQ_3:def 3;
  now
    let x be object;
A8: Re(r * f.x) = Re r * Re(f.x) - Im r * Im(f.x) by COMPLEX1:9;
    assume
A9: x in dom(r(#)(Re f));
    then
A10: (Re f).x = Re(f.x) by A1,COMSEQ_3:def 3;
    Re(r(#)f).x = Re((r(#)f).x) by A1,A6,A7,A4,A9,COMSEQ_3:def 3;
    then Re(r(#)f).x = r * Re(f.x) by A1,A6,A4,A5,A3,A9,A8,VALUED_1:def 5;
    hence (r(#)(Re f)).x = Re(r(#)f).x by A9,A10,VALUED_1:def 5;
  end;
  hence r(#)(Re f) = Re(r(#)f) by A1,A6,A7,A4,FUNCT_1:2;
A11: dom(r(#)(Im f)) = dom Im f by VALUED_1:def 5;
A12: dom Im f = dom f by COMSEQ_3:def 4;
A13: dom Im(r(#)f) = dom(r(#)f) by COMSEQ_3:def 4;
  now
    let x be object;
A14: Im(r * f.x) = Im r * Re(f.x) + Re r * Im(f.x) by COMPLEX1:9;
    assume
A15: x in dom(r(#)Im(f));
    then
A16: (Im f).x = Im(f.x) by A11,COMSEQ_3:def 4;
    Im(r(#)f).x = Im((r(#)f).x) by A11,A6,A13,A12,A15,COMSEQ_3:def 4;
    then Im(r(#)f).x = r * Im(f.x) by A11,A6,A12,A5,A3,A15,A14,VALUED_1:def 5;
    hence (r(#)Im(f)).x = Im(r(#)f).x by A15,A16,VALUED_1:def 5;
  end;
  hence thesis by A11,A6,A13,A12,FUNCT_1:2;
end;

theorem Th3:
  Re(c(#)f) = (Re c)(#)(Re f) - (Im c)(#)(Im f) & Im(c(#)f) = (Im c
  )(#)(Re f) + (Re c)(#)(Im f)
proof
A1: dom((Re c)(#)(Re f)) = dom Re f by VALUED_1:def 5;
A2: dom((Im c)(#)(Im f)) = dom Im f by VALUED_1:def 5;
A3: dom(c(#)f) = dom f by VALUED_1:def 5;
A4: dom(Re(c(#)f)) = dom(c(#)f) by COMSEQ_3:def 3;
A5: dom Re f = dom f by COMSEQ_3:def 3;
A6: dom Im f = dom f by COMSEQ_3:def 4;
A7: dom( Re(c)(#)Re(f) - Im(c)(#)Im(f) ) = dom(Re(c)(#)Re(f)) /\ dom(Im(c)
  (#)Im(f)) by VALUED_1:12;
  now
    let x be object;
A8: Re(c * f.x) = Re(c) * Re(f.x) - Im(c) * Im(f.x) by COMPLEX1:9;
    assume
A9: x in dom(Re(c(#)f));
    then
A10: (Im(c)(#)Im(f)).x = Im(c) * Im(f).x by A4,A6,A2,A3,VALUED_1:def 5;
A11: Im(f).x = Im(f.x) by A4,A6,A3,A9,COMSEQ_3:def 4;
A12: Re(f).x = Re(f.x) by A4,A5,A3,A9,COMSEQ_3:def 3;
    Re(c(#)f).x = Re((c(#)f).x) by A9,COMSEQ_3:def 3;
    then
A13: Re(c(#)f).x = Re(c * f.x) by A4,A9,VALUED_1:def 5;
    (Re(c)(#)Re(f)).x = Re(c) * Re(f).x by A4,A5,A1,A3,A9,VALUED_1:def 5;
    hence Re(c(#)f).x = ( Re(c)(#)Re(f) - Im(c)(#)Im(f) ).x by A4,A5,A6,A1,A2
,A3,A7,A9,A13,A10,A12,A11,A8,VALUED_1:13;
  end;
  hence Re(c(#)f) = Re(c)(#)Re(f) - Im(c)(#)Im(f) by A4,A5,A6,A1,A2,A3,A7,
FUNCT_1:2;
A14: dom((Im c)(#)(Re f)) = dom Re f by VALUED_1:def 5;
A15: dom((Re c)(#)(Im f)) = dom Im f by VALUED_1:def 5;
A16: dom(Im(c(#)f)) = dom(c(#)f) by COMSEQ_3:def 4;
A17: dom( Im(c)(#)Re(f) + Re(c)(#)Im(f) ) = dom(Im(c)(#)Re(f)) /\ dom(Re(c)
  (#)Im(f)) by VALUED_1:def 1;
  now
    let x be object;
    assume
A18: x in dom(Im(c(#)f));
    then
A19: (Im(c)(#)Re(f)).x = Im(c) * Re(f).x by A5,A16,A14,A3,VALUED_1:def 5;
    Im(c(#)f).x = Im((c(#)f).x) by A18,COMSEQ_3:def 4;
    then
A20: Im(c(#)f).x = Im(c * f.x) by A16,A18,VALUED_1:def 5;
A21: (Im f).x = Im(f.x) by A16,A6,A3,A18,COMSEQ_3:def 4;
A22: (Re f).x = Re(f.x) by A5,A16,A3,A18,COMSEQ_3:def 3;
A23: (Re(c)(#)Im(f)).x = Re(c) * Im(f).x by A16,A6,A15,A3,A18,VALUED_1:def 5;
    (Im(c)(#)Re(f) + Re(c)(#)Im(f)).x = (Im(c)(#)Re(f)).x + (Re(c)(#)Im(f
    )). x by A5,A16,A6,A14,A15,A3,A17,A18,VALUED_1:def 1;
    hence Im(c(#)f).x = ( Im(c)(#)Re(f) + Re(c)(#)Im(f) ).x by A20,A19,A23,A22
,A21,COMPLEX1:9;
  end;
  hence thesis by A5,A16,A6,A14,A15,A3,A17,FUNCT_1:2;
end;

theorem Th4:
  -(Im f) = Re(<i>(#)f) & Re f = Im(<i>(#)f)
proof
A1: dom -(Im f) = dom Im f by VALUED_1:8;
A2: dom(<i>(#)f) = dom f by VALUED_1:def 5;
A3: dom Im f = dom f by COMSEQ_3:def 4;
A4: dom Re(<i>(#)f) = dom(<i>(#)f) by COMSEQ_3:def 3;
  now
    let x be object;
A5: (-Im(f)).x = -((Im f).x) by VALUED_1:8;
A6: Re(<i> * f.x) = Re(<i>) * Re(f.x) - Im(<i>) * Im(f.x) by COMPLEX1:9;
    assume
A7: x in dom -(Im f);
    then Re(<i>(#)f).x = Re((<i>(#)f).x) by A1,A4,A2,A3,COMSEQ_3:def 3;
    then Re(<i>(#)f).x = -Im(f.x) by A1,A2,A3,A7,A6,COMPLEX1:7,VALUED_1:def 5;
    hence (-Im(f)).x = Re(<i>(#)f).x by A1,A7,A5,COMSEQ_3:def 4;
  end;
  hence -Im(f) = Re(<i>(#)f) by A4,A2,A3,FUNCT_1:2,VALUED_1:8;
A8: dom Re f = dom f by COMSEQ_3:def 3;
A9: dom Im(<i>(#)f) = dom(<i>(#)f) by COMSEQ_3:def 4;
  now
    let x be object;
A10: Im(<i> * f.x) = Im(<i>) * Re(f.x) + Re(<i>) * Im(f.x) by COMPLEX1:9;
    assume
A11: x in dom Re f;
    then Im(<i>(#)f).x = Im((<i>(#)f).x) by A8,A2,A9,COMSEQ_3:def 4;
    then Im(<i>(#)f).x = Re(f.x) by A8,A2,A11,A10,COMPLEX1:7,VALUED_1:def 5;
    hence Re(f).x = Im(<i>(#)f).x by A11,COMSEQ_3:def 3;
  end;
  hence thesis by A8,A2,A9,FUNCT_1:2;
end;

theorem Th5:
  Re(f+g) = Re f + Re g & Im(f+g) = Im f + Im g
proof
A1: dom(Re(f+g)) = dom(f+g) by COMSEQ_3:def 3;
A2: dom Re g = dom g by COMSEQ_3:def 3;
A3: dom Re f = dom f by COMSEQ_3:def 3;
  then dom((Re f)+(Re g)) = dom f /\ dom g by A2,VALUED_1:def 1;
  then
A4: dom(Re(f+g)) = dom((Re f)+(Re g)) by A1,VALUED_1:def 1;
  now
    let x be object;
    assume
A5: 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 A1,A5,VALUED_1:def 1;
    then
A6: Re(f+g).x = Re(f.x) + Re(g.x) by COMPLEX1:8;
A7: x in dom f /\ dom g by A1,A5,VALUED_1:def 1;
    then x in dom Re g by A2,XBOOLE_0:def 4;
    then
A8: (Re g).x = Re(g.x) by COMSEQ_3:def 3;
    x in dom Re f by A3,A7,XBOOLE_0:def 4;
    then (Re f).x = Re(f.x) by COMSEQ_3:def 3;
    hence Re(f+g).x = (Re(f)+Re(g)).x by A4,A5,A6,A8,VALUED_1:def 1;
  end;
  hence Re(f+g) = Re(f)+Re(g) by A4,FUNCT_1:2;
A9: dom Im(f+g) = dom(f+g) by COMSEQ_3:def 4;
A10: dom Im g = dom g by COMSEQ_3:def 4;
A11: dom Im f = dom f by COMSEQ_3:def 4;
  then dom(Im f + Im g) = dom f /\ dom g by A10,VALUED_1:def 1;
  then
A12: dom Im(f+g) = dom(Im f + Im g) by A9,VALUED_1:def 1;
  now
    let x be object;
    assume
A13: 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 A9,A13,VALUED_1:def 1;
    then
A14: Im(f+g).x = Im(f.x) + Im(g.x) by COMPLEX1:8;
A15: x in dom f /\ dom g by A9,A13,VALUED_1:def 1;
    then x in dom Im g by A10,XBOOLE_0:def 4;
    then
A16: (Im g).x = Im(g.x) by COMSEQ_3:def 4;
    x in dom Im f by A11,A15,XBOOLE_0:def 4;
    then (Im f).x = Im(f.x) by COMSEQ_3:def 4;
    hence Im(f+g).x = (Im(f)+Im(g)).x by A12,A13,A14,A16,VALUED_1:def 1;
  end;
  hence thesis by A12,FUNCT_1:2;
end;

theorem Th6:
  Re(f-g) = Re f - Re g & Im(f-g) = Im f - Im g
proof
  Re(f-g) = Re f + Re -g by Th5;
  then
A1: Re(f-g) = Re f + (-1)(#)(Re g) by Th2;
  Im(f-g) = Im f + Im -g by Th5;
  hence thesis by A1,Th2;
end;

theorem Th7: :: MESFUNC7:2
  (Re f)|A = Re(f|A) & (Im f)|A = Im(f|A)
proof
  dom((Re f)|A) = (dom Re f) /\ A by RELAT_1:61
    .= dom f /\ A by COMSEQ_3:def 3;
  then
A1: dom((Re f)|A) = dom(f|A) by RELAT_1:61
    .= dom Re(f|A) by COMSEQ_3:def 3;
  now
    let x be object;
    assume
A2: x in dom(Re(f)|A);
    then
A3: x in dom Re(f) /\ A by RELAT_1:61;
    then
A4: x in dom Re f by XBOOLE_0:def 4;
A5: x in A by A3,XBOOLE_0:def 4;
    thus Re(f|A).x = Re((f|A).x) by A1,A2,COMSEQ_3:def 3
      .= Re(f.x) by A5,FUNCT_1:49
      .= (Re f).x by A4,COMSEQ_3:def 3
      .= ((Re f)|A).x by A5,FUNCT_1:49;
  end;
  hence Re(f)|A = Re(f|A) by A1,FUNCT_1:2;
  dom((Im f)|A) = (dom Im f) /\ A by RELAT_1:61
    .= dom f /\ A by COMSEQ_3:def 4;
  then
A6: dom((Im f)|A) = dom(f|A) by RELAT_1:61
    .= dom Im(f|A) by COMSEQ_3:def 4;
  now
    let x be object;
    assume
A7: x in dom(Im(f)|A);
    then
A8: x in dom Im(f) /\ A by RELAT_1:61;
    then
A9: x in dom Im f by XBOOLE_0:def 4;
A10: x in A by A8,XBOOLE_0:def 4;
    thus Im(f|A).x = Im((f|A).x) by A6,A7,COMSEQ_3:def 4
      .= Im(f.x) by A10,FUNCT_1:49
      .= (Im f).x by A9,COMSEQ_3:def 4
      .= ((Im f)|A).x by A10,FUNCT_1:49;
  end;
  hence thesis by A6,FUNCT_1:2;
end;

theorem Th8:
  f = Re f + <i>(#)(Im f)
proof
A1: dom f = dom Re f by COMSEQ_3:def 3;
A2: dom f = dom Im f by COMSEQ_3:def 4;
A3: dom(Re f + <i>(#)(Im f)) = dom Re f /\ dom(<i>(#)(Im f)) by VALUED_1:def 1
    .= dom f /\ dom f by A1,A2,VALUED_1:def 5;
A4: dom(<i>(#)(Im f)) = dom Im f by VALUED_1:def 5;
  now
    let x be object;
    assume
A5: x in dom(Re f + <i>(#)(Im f));
    then (Re f + <i>(#)(Im f)).x = (Re f).x + (<i>(#)(Im f)).x by
VALUED_1:def 1
      .= Re(f.x) + (<i>(#)(Im f)).x by A1,A3,A5,COMSEQ_3:def 3
      .= Re(f.x) + <i> * (Im f).x by A2,A4,A3,A5,VALUED_1:def 5
      .= Re(f.x) + <i> * Im(f.x) by A2,A3,A5,COMSEQ_3:def 4;
    hence (Re f + <i>(#)(Im f)).x = f.x by COMPLEX1:13;
  end;
  hence thesis by A3,FUNCT_1:2;
end;

theorem
  B c= A & f is A-measurable implies f is B-measurable
by MESFUNC6:16;

theorem
  f is A-measurable & f is B-measurable implies f is (A\/B)-measurable
    by MESFUNC6:17;

theorem
  f is A-measurable & g is A-measurable implies f+g is A-measurable
proof
  assume that
A1: f is A-measurable and
A2: g is A-measurable;
A3: Im g is A-measurable by A2;
  Im f is A-measurable by A1;
  then Im f + Im g is A-measurable by A3,MESFUNC6:26;
  then
A4: Im(f+g) is A-measurable by Th5;
A5: Re g is A-measurable by A2;
  Re f is A-measurable by A1;
  then Re f + Re g is A-measurable by A5,MESFUNC6:26;
  then Re(f+g) is A-measurable by Th5;
  hence thesis by A4;
end;

theorem
  f is A-measurable & g is A-measurable & A c= dom g implies f-g
  is A-measurable
proof
  assume that
A1: f is A-measurable and
A2: g is A-measurable and
A3: A c= dom g;
A4: Im g is A-measurable by A2;
A5: A c= dom Re g by A3,COMSEQ_3:def 3;
A6: Re g is A-measurable by A2;
A7: A c= dom Im g by A3,COMSEQ_3:def 4;
  Im f is A-measurable by A1;
  then Im f - Im g is A-measurable by A4,A7,MESFUNC6:29;
  then
A8: Im(f-g) is A-measurable by Th6;
  Re f is A-measurable by A1;
  then Re f - Re g is A-measurable by A6,A5,MESFUNC6:29;
  then Re(f-g) is A-measurable by Th6;
  hence thesis by A8;
end;

theorem
  Y c= dom(f+g) implies dom(f|Y+g|Y)=Y & (f+g)|Y = f|Y+g|Y
proof
A1: dom(f+g) = dom f /\ dom g by VALUED_1:def 1;
  assume
A2: Y c= dom(f+g);
  then
A3: dom((f+g)|Y) = Y by RELAT_1:62;
  dom(g|Y) = dom g /\ Y by RELAT_1:61;
  then
A4: dom(g|Y) = Y by A2,A1,XBOOLE_1:18,28;
  dom(f|Y) = dom f /\ Y by RELAT_1:61;
  then
A5: dom(f|Y) = Y by A2,A1,XBOOLE_1:18,28;
  then
A6: dom(f|Y+g|Y) = Y /\ Y by A4,VALUED_1:def 1;
  now
    let x be object;
    assume
A7: x in dom((f+g)|Y);
    hence ((f+g)|Y).x = (f+g).x by FUNCT_1:47
      .=f.x+g.x by A2,A3,A7,VALUED_1:def 1
      .=(f|Y).x + g.x by A3,A5,A7,FUNCT_1:47
      .=(f|Y).x + (g|Y).x by A3,A4,A7,FUNCT_1:47
      .= ((f|Y)+(g|Y)).x by A3,A6,A7,VALUED_1:def 1;
  end;
  hence thesis by A2,A6,FUNCT_1:2,RELAT_1:62;
end;

theorem
  f is B-measurable & A = dom f /\ B implies f|B is A-measurable
proof
  assume that
A1: f is B-measurable and
A2: A = dom f /\ B;
A3: A = dom Im(f) /\ B by A2,COMSEQ_3:def 4;
  Im f is B-measurable by A1;
  then (Im f)|B is A-measurable by A3,MESFUNC6:76;
  then
A4: Im(f|B) is A-measurable by Th7;
A5: A = dom Re(f) /\ B by A2,COMSEQ_3:def 3;
  Re f is B-measurable by A1;
  then (Re f)|B is A-measurable by A5,MESFUNC6:76;
  then Re(f|B) is A-measurable by Th7;
  hence thesis by A4;
end;

theorem
  dom f in S & dom g in S implies dom(f+g) in S
proof
  assume that
A1: dom f in S and
A2: dom g in S;
  reconsider E1 = dom f, E2 = dom g as Element of S by A1,A2;
  dom(f+g) = E1 /\ E2 by VALUED_1:def 1;
  hence thesis;
end;

theorem
  dom f = A implies (f is B-measurable iff f is (A/\B)-measurable)
proof
  assume
A1: dom f = A;
  then
A2: dom Re f = A by COMSEQ_3:def 3;
A3: dom Im f = A by A1,COMSEQ_3:def 4;
  hence f is B-measurable implies f is (A/\B)-measurable by A2,MESFUNC6:80;
  thus thesis by A2,A3,MESFUNC6:80;
end;

theorem Th17:
  f is A-measurable & A c= dom f implies c(#)f is A-measurable
proof
  assume that
A1: f is A-measurable and
A2: A c= dom f;
A3: dom Im f = dom f by COMSEQ_3:def 4;
A4: Im f is A-measurable by A1;
  then
A5: Re(c)(#)Im(f) is A-measurable by A2,A3,MESFUNC6:21;
A6: Im(c)(#)Im(f) is A-measurable by A2,A4,A3,MESFUNC6:21;
A7: dom Re f = dom f by COMSEQ_3:def 3;
A8: Re f is A-measurable by A1;
  then Im(c)(#)Re(f) is A-measurable by A2,A7,MESFUNC6:21;
  then Im(c)(#)Re(f) + Re(c)(#)Im(f) is A-measurable by A5,MESFUNC6:26;
  then
A9: Im(c(#)f) is A-measurable by Th3;
  dom(Im(c)(#)Im(f)) = dom Im(f) by VALUED_1:def 5;
  then
A10: A c= dom(Im(c)(#)Im(f)) by A2,COMSEQ_3:def 4;
  Re(c)(#)Re(f) is A-measurable by A2,A8,A7,MESFUNC6:21;
  then Re(c)(#)Re(f) - Im(c)(#)Im(f) is A-measurable by A6,A10,MESFUNC6:29;
  then Re(c(#)f) is A-measurable by Th3;
  hence thesis by A9;
end;

theorem
  ( ex A be Element of S st dom f = A ) implies for c be Complex,
  B be Element of S st f is B-measurable holds c(#)f is B-measurable
proof
  assume ex A be Element of S st A = dom f;
  then consider A be Element of S such that
A1: A = dom f;
  hereby
    let c be Complex, B be Element of S;
A2: dom((Re c)(#)(Re f)) = dom Re f by VALUED_1:def 5;
A3: dom((Im c)(#)(Im f)) = dom Im f by VALUED_1:def 5;
    dom(Re(c(#)f)) = dom((Re c)(#)(Re f) - (Im c)(#)(Im f)) by Th3;
    then
A4: dom(Re(c(#)f)) = dom((Re c)(#)(Re f)) /\ dom((Im c)(#)(Im f)) by
VALUED_1:12;
A5: dom((Im c)(#)(Re f)) = dom Re f by VALUED_1:def 5;
    dom(Im(c(#)f)) = dom((Im c)(#)(Re f) + (Re c)(#)(Im f)) by Th3;
    then
A6: dom(Im(c(#)f)) = dom((Im c)(#)(Re f)) /\ dom((Re c)(#)(Im f)) by
VALUED_1:def 1;
A7: dom((Re c)(#)(Im f)) = dom Im f by VALUED_1:def 5;
A8: dom Re f = dom f by COMSEQ_3:def 3;
A9: dom Im f = dom f by COMSEQ_3:def 4;
    assume
A10: f is B-measurable;
    then Im f is B-measurable;
    then
A11: Im f is (A/\B)-measurable by A1,A9,MESFUNC6:80;
    Re f is B-measurable by A10;
    then Re f is (A/\B)-measurable by A1,A8,MESFUNC6:80;
    then f is (A/\B)-measurable by A11;
    then
A12: c(#)f is (A/\B)-measurable by A1,Th17,XBOOLE_1:17;
    then Im(c(#)f) is (A/\B)-measurable;
    then
A13: Im(c(#)f) is B-measurable by A1,A8,A9,A5,A7,A6,MESFUNC6:80;
    Re(c(#)f) is (A/\B)-measurable by A12;
    then Re(c(#)f) is B-measurable by A1,A8,A9,A2,A3,A4,MESFUNC6:80;
    hence c(#)f is B-measurable by A13;
  end;
end;

begin :: The Integral of a Complex-valued Measurable Function

definition
  let X be non empty set;
  let S be SigmaField of X;
  let M be sigma_Measure of S;
  let f be PartFunc of X,COMPLEX;
  pred f is_integrable_on M means
  Re f is_integrable_on M & Im f is_integrable_on M;
end;

definition
  let X be non empty set;
  let S be SigmaField of X;
  let M be sigma_Measure of S;
  let f be PartFunc of X,COMPLEX;
  assume
A1: f is_integrable_on M;
  func Integral(M,f) -> Complex means
  :Def3:
  ex R,I be Real st R =
  Integral(M,Re f) & I = Integral(M,Im f) & it = R+ I*<i>;
  existence
  proof
A2: Im f is_integrable_on M by A1;
    then
A3: -infty < Integral(M,Im f) by MESFUNC6:90;
A4: Re f is_integrable_on M by A1;
    then
A5: Integral(M,Re f) < +infty by MESFUNC6:90;
A6: Integral(M,Im f) < +infty by A2,MESFUNC6:90;
    -infty < Integral(M,Re f) by A4,MESFUNC6:90;
    then reconsider R=Integral(M,Re f), I=Integral(M,Im f)
as Element of REAL by A5,A3,A6,
XXREAL_0:14;
    take R + I*<i>;
    thus thesis;
  end;
  uniqueness;
end;

Lm1: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f
be PartFunc of X,ExtREAL holds max+f is nonnegative & max-f is nonnegative
proof
  let X be non empty set;
  let S be SigmaField of X;
  let M be sigma_Measure of S;
  let f be PartFunc of X,ExtREAL;
A1: for x be object st x in dom max- f holds 0<= (max-f).x by MESFUNC2:13;
  for x be object st x in dom max+ f holds 0<= (max+f).x by MESFUNC2:12;
  hence thesis by A1,SUPINF_2:52;
end;

theorem Th19:
  for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, A be Element of S st (ex E be Element of S st
  E = dom f & f is E-measurable) & M.A = 0 holds f|A 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,ExtREAL, A be Element of S;
  assume that
A1: ex E be Element of S st E = dom f & f is E-measurable and
A2: M.A = 0;
A3: dom f=dom (max+ f) by MESFUNC2:def 2;
  max+f is nonnegative by Lm1;
  then integral+(M,(max+ f)|A)=0 by A1,A2,A3,MESFUNC2:25,MESFUNC5:82;
  then
A4: integral+(M,max+(f|A)) < +infty by MESFUNC5:28;
  consider E be Element of S such that
A5: E = dom f and
A6: f is E-measurable by A1;
A7: dom f /\ (A /\ E) = A /\ E by A5,XBOOLE_1:17,28;
A8: dom f=dom (max- f) by MESFUNC2:def 3;
  max-f is nonnegative by Lm1;
  then integral+(M,(max- f)|A)=0 by A1,A2,A8,MESFUNC2:26,MESFUNC5:82;
  then
A9: integral+(M,max-(f|A)) < +infty by MESFUNC5:28;
A10: dom (f|A) = dom f /\ A by RELAT_1:61;
  f is (A/\E)-measurable by A6,MESFUNC1:30,XBOOLE_1:17;
  then
A11: f|(A /\ E) is (A/\E)-measurable by A7,MESFUNC5:42;
  f|(A /\ E) = f|A /\ f|E by RELAT_1:79
    .= f|A /\ f by A5
    .= f|A by RELAT_1:59,XBOOLE_1:28;
  hence thesis by A5,A11,A10,A4,A9;
end;

theorem Th20:
  for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,REAL, E,A be Element of S st (ex E be Element of S st
  E = dom f & f is E-measurable) & M.A = 0 holds f|A is_integrable_on M
by Th19;

theorem
  (ex E be Element of S st E = dom f & f is E-measurable) & M.A = 0
  implies f|A is_integrable_on M & Integral(M,f|A) = 0
proof
  set g = f|A;
  assume that
A1: ex E be Element of S st E = dom f & f is E-measurable and
A2: M.A = 0;
  consider E be Element of S such that
A3: E = dom f and
A4: f is E-measurable by A1;
A5: dom Im f = dom f by COMSEQ_3:def 4;
A6: Im f is E-measurable by A4;
  then
A7: Integral(M,Im(f)|A)=0 by A2,A3,A5,MESFUNC6:88;
  (Im f)|A is_integrable_on M by A2,A3,A6,A5,Th20;
  then
A8: Im g is_integrable_on M by Th7;
A9: dom Re f = dom f by COMSEQ_3:def 3;
A10: Im g = (Im f)|A by Th7;
A11: Re f is E-measurable by A4;
A12: Re g = (Re f)|A by Th7;
  then reconsider
  R=Integral(M,Re g), I=Integral(M,Im g) as Real by A2,A3,A11,A6,A9,A5,A10,
MESFUNC6:88;
  (Re f)|A is_integrable_on M by A2,A3,A11,A9,Th20;
  then Re g is_integrable_on M by Th7;
  hence g is_integrable_on M by A8;
  hence Integral(M,g) = R + I * <i> by Def3
    .= 0 by A2,A3,A11,A9,A7,A12,A10,MESFUNC6:88;
end;

theorem
  E = dom f & f is_integrable_on M & M.A =0 implies Integral(M,f|(E\A))
  = Integral(M,f)
proof
  assume that
A1: E = dom f and
A2: f is_integrable_on M and
A3: M.A =0;
  set C=E\A;
A4: dom f = dom Re f by COMSEQ_3:def 3;
A5: Im f is_integrable_on M by A2;
  then R_EAL(Im f) is_integrable_on M;
  then consider IE be Element of S such that
A6: IE = dom(R_EAL(Im f)) and
A7: R_EAL(Im f) is IE-measurable;
A8: dom f = dom Im f by COMSEQ_3:def 4;
A9: Integral(M,Im(f)|C) = Integral(M,Im(f|C)) by Th7;
  Im f is IE-measurable by A7;
  then
A10: Integral(M,Im(f|C)) = Integral(M,Im f) by A1,A3,A8,A6,A9,MESFUNC6:89;
  (Im f)|C is_integrable_on M by A5,MESFUNC6:91;
  then
A11: Im(f|C) is_integrable_on M by Th7;
  then
A12: -infty < Integral(M,Im(f|C)) by MESFUNC6:90;
A13: Re f is_integrable_on M by A2;
  then R_EAL(Re f) is_integrable_on M;
  then consider RE be Element of S such that
A14: RE = dom(R_EAL(Re f)) and
A15: R_EAL(Re f) is RE-measurable;
A16: Integral(M,Re(f)|C) = Integral(M,Re(f|C)) by Th7;
  Re f is RE-measurable by A15;
  then
A17: Integral(M,Re(f|C)) = Integral(M,Re f) by A1,A3,A4,A14,A16,MESFUNC6:89;
  (Re f)|C is_integrable_on M by A13,MESFUNC6:91;
  then
A18: Re(f|C) is_integrable_on M by Th7;
  then
A19: Integral(M,Re(f|C)) < +infty by MESFUNC6:90;
A20: Integral(M,Im(f|C)) < +infty by A11,MESFUNC6:90;
  -infty < Integral(M,Re(f|C)) by A18,MESFUNC6:90;
  then reconsider R2=Integral(M,Re(f|C)), I2=Integral(M,Im(f|C))
as Element of REAL by A19
,A12,A20,XXREAL_0:14;
  f|(E\A) is_integrable_on M by A18,A11;
  hence Integral(M,f|(E\A)) = R2 + I2 * <i> by Def3
    .= Integral(M,f) by A2,A17,A10,Def3;
end;

theorem Th23:
  f is_integrable_on M implies f|A is_integrable_on M
proof
  assume
A1: f is_integrable_on M;
  then Im f is_integrable_on M;
  then (Im f)|A is_integrable_on M by MESFUNC6:91;
  then
A2: Im(f|A) is_integrable_on M by Th7;
  Re f is_integrable_on M by A1;
  then (Re f)|A is_integrable_on M by MESFUNC6:91;
  then Re(f|A) is_integrable_on M by Th7;
  hence thesis by A2;
end;

theorem
  f is_integrable_on M & A misses B implies Integral(M,f|(A\/B)) =
  Integral(M,f|A) + Integral(M,f|B)
proof
  assume that
A1: f is_integrable_on M and
A2: A misses B;
A3: f|B is_integrable_on M by A1,Th23;
  then
A4: Re(f|B) is_integrable_on M;
  then
A5: Integral(M,Re(f|B)) < +infty by MESFUNC6:90;
A6: Im(f|B) is_integrable_on M by A3;
  then
A7: -infty < Integral(M,Im(f|B)) by MESFUNC6:90;
A8: Integral(M,Im(f|B)) < +infty by A6,MESFUNC6:90;
  -infty < Integral(M,Re(f|B)) by A4,MESFUNC6:90;
  then reconsider R2=Integral(M,Re(f|B)), I2=Integral(M,Im(f|B))
as Element of REAL by A5
,A7,A8,XXREAL_0:14;
A9: f|A is_integrable_on M by A1,Th23;
  then
A10: Re(f|A) is_integrable_on M;
  then
A11: Integral(M,Re(f|A)) < +infty by MESFUNC6:90;
  set C=A\/B;
A12: f|(A\/B) is_integrable_on M by A1,Th23;
  then
A13: Re(f|C) is_integrable_on M;
  then
A14: Integral(M,Re(f|C)) < +infty by MESFUNC6:90;
A15: Im(f|C) is_integrable_on M by A12;
  then
A16: -infty < Integral(M,Im(f|C)) by MESFUNC6:90;
A17: Integral(M,Im(f|C)) < +infty by A15,MESFUNC6:90;
  -infty < Integral(M,Re(f|C)) by A13,MESFUNC6:90;
  then reconsider R3=Integral(M,Re(f|C)), I3=Integral(M,Im(f|C))
as Element of REAL
  by A14,A16,A17,XXREAL_0:14;
A18: Integral(M,f|(A\/B)) = R3 + I3 * <i> by A12,Def3;
A19: Im(f|A) is_integrable_on M by A9;
  then
A20: -infty < Integral(M,Im(f|A)) by MESFUNC6:90;
A21: Integral(M,Im(f|A)) < +infty by A19,MESFUNC6:90;
  -infty < Integral(M,Re(f|A)) by A10,MESFUNC6:90;
  then reconsider R1=Integral(M,Re(f|A)), I1=Integral(M,Im(f|A))
as Element of REAL by A11
,A20,A21,XXREAL_0:14;
  Im f is_integrable_on M by A1;
  then
  Integral(M,(Im f)|(A\/B)) = Integral(M,(Im f)|A) + Integral(M,(Im f)|B)
  by A2,MESFUNC6:92;
  then Integral(M,Im(f)|C) = Integral(M,Im(f|A)) + Integral(M,Im(f)|B) by Th7
    .= Integral(M,Im(f|A)) + Integral(M,Im(f|B)) by Th7;
  then I3 = I1 + (I2 qua ExtReal) by Th7;
  then
A22: I3 = I1 + I2;
  Re f is_integrable_on M by A1;
  then
  Integral(M,(Re f)|(A\/B)) = Integral(M,(Re f)|A) + Integral(M,(Re f)|B)
  by A2,MESFUNC6:92;
  then Integral(M,Re(f)|C) = Integral(M,Re(f|A)) + Integral(M,Re(f)|B) by Th7
    .= Integral(M,Re(f|A)) + Integral(M,Re(f|B)) by Th7;
  then R3 = R1 + (R2 qua ExtReal) by Th7;
  then R3 = R1 + R2;
  then Integral(M,f|(A\/B)) = (R1 + I1 * <i>) + (R2 + I2 * <i>) by A22,A18;
  then Integral(M,f|(A\/B)) = Integral(M,f|A) + (R2 + I2 * <i>) by A9,Def3;
  hence thesis by A3,Def3;
end;

theorem
  f is_integrable_on M & B = (dom f)\A implies f|A is_integrable_on M &
  Integral(M,f) = Integral(M,f|A)+Integral(M,f|B)
proof
  assume that
A1: f is_integrable_on M and
A2: B = (dom f)\A;
A3: Re f is_integrable_on M by A1;
  then
A4: Integral(M,Re f) < +infty by MESFUNC6:90;
A5: Im f is_integrable_on M by A1;
  then
A6: -infty < Integral(M,Im f) by MESFUNC6:90;
A7: Integral(M,Im f) < +infty by A5,MESFUNC6:90;
  -infty < Integral(M,Re f) by A3,MESFUNC6:90;
  then reconsider R=Integral(M,Re f), I=Integral(M,Im f)
as Element of REAL by A4,A6,A7,
XXREAL_0:14;
A8: Integral(M,f) = R + I * <i> by A1,Def3;
A9: f|B is_integrable_on M by A1,Th23;
  then
A10: Re(f|B) is_integrable_on M;
  then
A11: Integral(M,Re(f|B)) < +infty by MESFUNC6:90;
A12: Im(f|B) is_integrable_on M by A9;
  then
A13: -infty < Integral(M,Im(f|B)) by MESFUNC6:90;
A14: Integral(M,Im(f|B)) < +infty by A12,MESFUNC6:90;
  -infty < Integral(M,Re(f|B)) by A10,MESFUNC6:90;
  then reconsider R2=Integral(M,Re(f|B)), I2=Integral(M,Im(f|B))
as Element of REAL by A11
,A13,A14,XXREAL_0:14;
A15: f|A is_integrable_on M by A1,Th23;
  then
A16: Re(f|A) is_integrable_on M;
  then
A17: Integral(M,Re(f|A)) < +infty by MESFUNC6:90;
A18: Im(f|A) is_integrable_on M by A15;
  then
A19: -infty < Integral(M,Im(f|A)) by MESFUNC6:90;
A20: Integral(M,Im(f|A)) < +infty by A18,MESFUNC6:90;
  -infty < Integral(M,Re(f|A)) by A16,MESFUNC6:90;
  then reconsider R1=Integral(M,Re(f|A)), I1=Integral(M,Im(f|A))
as Element of REAL by A17
,A19,A20,XXREAL_0:14;
  dom f = dom Im f by COMSEQ_3:def 4;
  then Integral(M,Im(f)) = Integral(M,Im(f)|A)+Integral(M,Im(f)|B) by A2,A5,
MESFUNC6:93;
  then Integral(M,Im f) = Integral(M,Im(f|A)) + Integral(M,Im(f)|B) by Th7
    .= Integral(M,Im(f|A)) + Integral(M,Im(f|B)) by Th7;
  then
A21: I = I1 + I2 by SUPINF_2:1;
  dom f = dom Re f by COMSEQ_3:def 3;
  then Integral(M,Re(f)) = Integral(M,Re(f)|A)+Integral(M,Re(f)|B) by A2,A3,
MESFUNC6:93;
  then Integral(M,Re f) = Integral(M,Re(f|A)) + Integral(M,Re(f)|B) by Th7
    .= Integral(M,Re(f|A)) + Integral(M,Re(f|B)) by Th7;
  then R = R1 + R2 by SUPINF_2:1;
  then Integral(M,f) = (R1 + I1 * <i>) + (R2 + I2 * <i>) by A21,A8;
  then Integral(M,f) = Integral(M,f|A) + (R2 + I2 * <i>) by A15,Def3;
  hence thesis by A1,A9,Def3,Th23;
end;

definition
  let k be Real, X be non empty set, f be PartFunc of X,REAL;
  func f to_power k -> PartFunc of X,REAL means
  :Def4:
  dom it = dom f & for x
  be Element of X st x in dom it holds it.x = (f.x) to_power k;
  existence
  proof
    defpred P[set,set] means $1 in dom f & $2= (f.$1) to_power k;
    consider F be PartFunc of X,REAL such that
A1: for z be Element of X holds z in dom F iff ex c be Element of REAL
    st P[z,c] and
A2: for z be Element of X st z in dom F holds P[z,F.z] from SEQ_1:sch
    2;
    take F;
    now
      let z be Element of X;
      hereby
A3:     (f.z) to_power k is Element of REAL by XREAL_0:def 1;
        assume z in dom f;
        hence z in dom F by A1,A3;
      end;
      hereby
        assume z in dom F;
        then ex c be Element of REAL st P[z,c] by A1;
        hence z in dom f;
      end;
    end;
    hence dom F = dom f by SUBSET_1:3;
    thus thesis by A2;
  end;
  uniqueness
  proof
    deffunc f0(set) = (f.$1) to_power k;
    thus for h,g being PartFunc of X,REAL st (dom h=dom f & for z be Element
of X st z in dom h holds h.z = f0(z)) & (dom g=dom f & for z be Element of X st
    z in dom g holds g.z = f0(z)) holds h = g from SEQ_1:sch 4;
  end;
end;

registration
  let X;
  cluster nonnegative for PartFunc of X,REAL;
  existence
  proof
    reconsider f = {} as Function;
    reconsider f as PartFunc of X,REAL by RELSET_1:12;
    take f;
    let x be ExtReal;
    thus thesis;
  end;
end;

registration
  let k be non negative Real, X;
  let f be nonnegative PartFunc of X,REAL;
  cluster f to_power k -> nonnegative;
  coherence
  proof
    now
      let x be object;
      assume
A1:   x in dom (f to_power k);
      per cases;
      suppose
        k = 0;
        then (f.x) to_power k = 1 by POWER:24;
        hence 0 <= (f to_power k).x by A1,Def4;
      end;
      suppose
A2:     k > 0;
        per cases by MESFUNC6:51;
        suppose
          0 < f.x;
          then 0 < (f.x) to_power k by POWER:34;
          hence 0 <= (f to_power k).x by A1,Def4;
        end;
        suppose
          0 = f.x;
          then 0 = ((f.x) to_power k) by A2,POWER:def 2;
          hence 0 <= (f to_power k).x by A1,Def4;
        end;
      end;
    end;
    hence thesis by MESFUNC6:52;
  end;
end;

theorem Th26:
  for k be Real, X,S,E for f be PartFunc of X,REAL st f is
  nonnegative & 0 <= k holds (f to_power k) is nonnegative;

theorem Th27:
  for x be object,X,S,E for f be PartFunc of X,REAL st f is
  nonnegative holds (f.x) to_power (1/2) = sqrt(f.x)
proof
  let x be object,X,S,E;
  let f be PartFunc of X,REAL;
  assume f is nonnegative;
  then
A1: 0 <= f.x by MESFUNC6:51;
  hence (f.x) to_power (1/2) = 2-root (f.x) by POWER:45
    .= 2 -Root (f.x) by A1,POWER:def 1
    .= sqrt (f.x) by A1,PREPOWER:32;
end;

theorem Th28:
  for f be PartFunc of X,REAL, a be Real st A c= dom f holds A /\
  less_dom(f,a) = A\(A /\ great_eq_dom(f,a))
proof
  let f be PartFunc of X,REAL, a be Real;
  now
    let x be object;
    assume
A1: x in A /\ less_dom(f,a);
    then x in less_dom(f,a) by XBOOLE_0:def 4;
    then ex y be Real st y = f.x & y < a by MESFUNC6:3;
    then not (ex y1 be Real st y1 = f.x & a <= y1);
    then not x in great_eq_dom(f,a) by MESFUNC6:6;
    then
A2: not x in (A /\ great_eq_dom(f,a)) by XBOOLE_0:def 4;
    x in A by A1,XBOOLE_0:def 4;
    hence x in A\(A /\ great_eq_dom(f,a)) by A2,XBOOLE_0:def 5;
  end;
  then
A3: A /\ less_dom(f,a) c= A\(A /\ great_eq_dom(f,a)) by TARSKI:def 3;
  assume
A4: A c= dom f;
  now
    let x be object;
    assume
A5: x in A\(A /\ great_eq_dom(f,a));
    then
A6: x in A by XBOOLE_0:def 5;
    not x in A /\ great_eq_dom(f,a) by A5,XBOOLE_0:def 5;
    then not x in great_eq_dom(f,a) by A6,XBOOLE_0:def 4;
    then not a <= f.x by A4,A6,MESFUNC6:6;
    then x in less_dom(f,a) by A4,A6,MESFUNC6:3;
    hence x in A /\ less_dom(f,a) by A6,XBOOLE_0:def 4;
  end;
  then A\(A /\ great_eq_dom(f,a)) c= A /\ less_dom(f,a) by TARSKI:def 3;
  hence thesis by A3,XBOOLE_0:def 10;
end;

reconsider jj=1 as Real;

theorem Th29:
  for k be Real, X,S,E for f be PartFunc of X,REAL st f is
  nonnegative & 0 <= k & E c= dom f & f is E-measurable holds (f to_power k)
  is E-measurable
proof
  let k be Real, X,S,E;
  let f be PartFunc of X,REAL;
  reconsider k1=k as Real;
  assume that
A1: f is nonnegative and
A2: 0 <= k and
A3: E c= dom f and
A4: f is E-measurable;
A5: dom(f to_power k) = dom f by Def4;
  per cases by A2;
  suppose
A6: k = 0;
A7: E c= dom (f to_power k) by A3,Def4;
    now
      let r be Real;
      reconsider r1=r as Real;
      per cases;
      suppose
A8:     r <= 1;
        now
          let x be object;
          assume
A9:       x in E;
          then (f to_power k).x = (f.x) to_power k by A3,A5,Def4;
          then r <= (f to_power k).x by A6,A8,POWER:24;
          hence x in great_eq_dom(f to_power k,r1) by A3,A5,A9,MESFUNC6:6;
        end;
        then E c= great_eq_dom(f to_power k,r) by TARSKI:def 3;
        then E /\ great_eq_dom(f to_power k,r) = E by XBOOLE_1:28;
        then E /\ less_dom(f to_power k,r1) = E \ E by A7,Th28;
        hence E /\ less_dom(f to_power k,r) in S;
      end;
      suppose
A10:    1 < r;
        now
          let x be object;
          assume
A11:      x in E;
          then (f to_power k).x = (f.x) to_power k by A3,A5,Def4;
          then (f to_power k).x < r by A6,A10,POWER:24;
          hence x in less_dom(f to_power k,r) by A3,A5,A11,MESFUNC6:3;
        end;
        then E c= less_dom(f to_power k,r) by TARSKI:def 3;
        then E /\ less_dom(f to_power k,r) = E by XBOOLE_1:28;
        hence E /\ less_dom(f to_power k,r) in S;
      end;
    end;
    hence thesis by MESFUNC6:12;
  end;
  suppose
A12: k > 0;
    for r be Real holds E /\ great_eq_dom(f to_power k,r) in S
    proof
      let r be Real;
      reconsider r1=r as Real;
      per cases;
      suppose
A13:    r1 <= 0;
        now
          let x be object;
          assume x in E;
          then x in dom f by A3;
          then
A14:      x in dom (f to_power k) by Def4;
          0 <= (f to_power k).x by A1,A12,MESFUNC6:51;
          hence x in great_eq_dom(f to_power k,r1) by A13,A14,MESFUNC6:6;
        end;
        then E c= great_eq_dom(f to_power k,r) by TARSKI:def 3;
        then E /\ great_eq_dom(f to_power k,r) = E by XBOOLE_1:28;
        hence thesis;
      end;
      suppose
A15:    0 < r1;
A16:    now
          set R = r to_power (jj/k);
          let x be object;
           reconsider xx=x as set by TARSKI:1;
A17:      0 < r to_power (jj/k) by A15,POWER:34;
          assume
A18:      x in great_eq_dom(f,r1 to_power (1/k));
          then
A19:      x in dom (f to_power k) by A5,MESFUNC6:6;
          R to_power k = r to_power (1/k*k) by A15,POWER:33;
          then
A20:      R to_power k = r to_power 1 by A12,XCMPLX_1:87;
          ex y be Real st y = f.x & r1 to_power (1/k) <= y
              by A18,MESFUNC6:6;
          then r1 to_power jj <= (f.xx) to_power k1
                 by A12,A17,A20,HOLDER_1:3;
          then r <= (f.xx) to_power k by POWER:25;
          then r <= (f to_power k).xx by A19,Def4;
          hence x in great_eq_dom(f to_power k,r1) by A19,MESFUNC6:6;
        end;
        now
          let x be object;
           reconsider xx=x as set by TARSKI:1;
          assume
A21:      x in great_eq_dom(f to_power k,r1);
          then
A22:      x in dom (f to_power k) by MESFUNC6:6;
          0 <= f.xx by A1,MESFUNC6:51;
          then
          ((f.xx) to_power k1) to_power (1/k1) = (f.xx) to_power (k1 * 1/k1
          ) by A12,HOLDER_1:2;
          then ((f.xx) to_power k1) to_power (1/k1) = (f.xx) to_power 1 by A12,
XCMPLX_1:87;
          then
A23:      ((f.xx) to_power k) to_power (1/k) = f.x by POWER:25;
          ex y2 be Real st y2 = (f to_power k).x & r1 <= y2
by A21,MESFUNC6:6;
          then r <= (f.xx) to_power k by A22,Def4;
          then
          r to_power (1/k1) <= ((f.xx) to_power k1) to_power (1/k1) by A12,A15,
HOLDER_1:3;
          hence x in great_eq_dom(f,r1 to_power (1/k)) by A5,A22,A23,MESFUNC6:6
;
        end;
        then E /\ great_eq_dom(f to_power k,r1) = E /\ great_eq_dom(f,r1
        to_power (1/k)) by A16,TARSKI:2;
        hence thesis by A3,A4,MESFUNC6:13;
      end;
    end;
    hence thesis by A3,A5,MESFUNC6:13;
  end;
end;

theorem Th30:
  f is A-measurable & A c= dom f implies |.f.| is A-measurable
proof
  assume that
A1: f is A-measurable and
A2: A c= dom f;
A3: dom Im f = dom f by COMSEQ_3:def 4;
A4: now
    let x be object;
    assume x in dom |.Im f.|;
     then |.Im f.|.x = |.(Im f).x qua Complex .| by VALUED_1:def 11;
    hence 0 <= |.Im f.|.x by COMPLEX1:46;
  end;
  then
A5: |.Im f.| to_power 2 is nonnegative by Th26,MESFUNC6:52;
A6: dom |.Im f.| = dom Im f by VALUED_1:def 11;
  then
A7: dom(|.Im f.| to_power 2) = dom f by A3,Def4;
  Im f is A-measurable by A1;
  then |.Im f.| is A-measurable by A2,A3,MESFUNC6:48;
  then
A8: |.Im f.| to_power 2 is A-measurable by A2,A6,A3,A4,Th29,MESFUNC6:52;
A9: dom Re f = dom f by COMSEQ_3:def 3;
A10: now
    let x be object;
A11: 0 <= |.(Re f).x qua Complex .| by COMPLEX1:46;
    assume x in dom |.Re f.|;
    hence 0 <= |. Re f.|.x by A11,VALUED_1:def 11;
  end;
  then
A12: |.Re(f).| to_power 2 is nonnegative by Th26,MESFUNC6:52;
  set F = |.Re f.| to_power 2 + |.Im f.| to_power 2;
A13: dom |.f.| = dom f by VALUED_1:def 11;
A14: dom |.Re f.| = dom Re f by VALUED_1:def 11;
  then
A15: dom(|.Re f.| to_power 2) = dom f by A9,Def4;
A16: dom F = dom( |.Re f.| to_power 2 ) /\ dom( |.Im f.| to_power 2 ) by
VALUED_1:def 1;
  then
A17: dom(|.f.|) = dom (F to_power (1/2)) by A13,A15,A7,Def4;
  now
    let x be object;
    assume
A18: x in dom |.f.|;
    then (|.Re f.| to_power 2).x = (|.Re f.|.x) to_power 2 by A13,A15,Def4;
    then (|.Re f.| to_power 2).x
        = |.Re(f).x qua Complex .| to_power 2 by A14,A13,A9,A18,
VALUED_1:def 11;
    then (|.Re f.| to_power 2).x =
      |.Re(f.x) qua Complex.| to_power 2 by A13,A9,A18,
COMSEQ_3:def 3;
    then (|.Re f.| to_power 2).x = |.Re(f.x) qua Complex.|^2 by POWER:46;
    then
A19: (|.Re f.| to_power 2).x = (Re(f.x))^2 by COMPLEX1:75;
    (|.Im f.| to_power 2).x = (|.Im f.|.x) to_power 2 by A13,A7,A18,Def4;
    then (|.Im f.| to_power 2).x
          = |.Im(f).x qua Complex .| to_power 2 by A6,A13,A3,A18,
VALUED_1:def 11;
    then (|.Im f.| to_power 2).x
          = |.Im(f.x) qua Complex.| to_power 2 by A13,A3,A18,
COMSEQ_3:def 4;
    then (|.Im f.| to_power 2).x = |.Im(f.x) qua Complex.|^2 by POWER:46;
    then
A20: (|.Im f.| to_power 2).x = (Im(f.x))^2 by COMPLEX1:75;
    (F.x) to_power (1/2) = sqrt (F.x) by A12,A5,Th27,MESFUNC6:56
      .= sqrt ( (Re(f.x))^2 + (Im(f.x))^2 ) by A13,A16,A15,A7,A18,A19,A20,
VALUED_1:def 1;
    then (F to_power (1/2)).x = |.f.x .| by A17,A18,Def4;
    hence |.f.|.x = (F to_power (1/2)).x by A18,VALUED_1:def 11;
  end;
  then
A21: |.f.| = F to_power (1/2) by A17,FUNCT_1:2;
  Re f is A-measurable by A1;
  then |.Re f.| is A-measurable by A2,A9,MESFUNC6:48;
  then |.Re f.| to_power 2 is A-measurable by A2,A14,A9,A10,Th29,MESFUNC6:52
;
  then F is A-measurable by A8,MESFUNC6:26;
  hence thesis by A2,A12,A5,A16,A15,A7,A21,Th29,MESFUNC6:56;
end;

theorem Th31:
  (ex A be Element of S st A = dom f & f is A-measurable )
  implies (f is_integrable_on M iff |.f.| is_integrable_on M)
proof
A1: dom (|.Re f.| + |.Im f.|) = dom |.Re f.| /\ dom |.Im f.| by VALUED_1:def 1;
A2: dom |.Re f.| = dom Re f by VALUED_1:def 11;
A3: dom |.Im f.| = dom Im f by VALUED_1:def 11;
A4: dom |.f.| = dom f by VALUED_1:def 11;
  assume ex A be Element of S st A = dom f & f is A-measurable;
  then consider A be Element of S such that
A5: A = dom f and
A6: f is A-measurable;
A7: dom Re f = A by A5,COMSEQ_3:def 3;
A8: Im f is A-measurable by A6;
A9: Re f is A-measurable by A6;
A10: dom Im f = A by A5,COMSEQ_3:def 4;
A11: |.f.| is A-measurable by A5,A6,Th30;
  hereby
A12: now
      let x be Element of X;
      assume
A13:  x in dom |.f.|;
      then
A14:  |.f.|.x = |.f.x .| by VALUED_1:def 11;
A15:  |.(Im f).x qua Complex .| = |.Im f.|.x
          by A5,A10,A3,A4,A13,VALUED_1:def 11;
A16:  |.(Re f).x qua Complex .| = |.Re f.|.x
           by A5,A7,A2,A4,A13,VALUED_1:def 11;
A17:  (Im f).x = Im(f.x) by A5,A10,A4,A13,COMSEQ_3:def 4;
A18:  (Re f).x = Re(f.x) by A5,A7,A4,A13,COMSEQ_3:def 3;
      (|.Re f.| + |.Im f.|).x = |.Re f.|.x + |.Im f.|.x by A5,A7,A10,A1,A2,A3
,A4,A13,VALUED_1:def 1;
      hence |.(|.f.|.x  qua Complex).|
     <= (|.Re f.| + |.Im f.|).x by A18,A17,A14,A16,A15,
COMPLEX1:78;
    end;
    assume
A19: f is_integrable_on M;
    then Im f is_integrable_on M;
    then
A20: |.Im f.| is_integrable_on M by A10,A8,MESFUNC6:94;
    Re f is_integrable_on M by A19;
    then |.Re f.| is_integrable_on M by A7,A9,MESFUNC6:94;
    then |.Re f.| + |.Im f.| is_integrable_on M by A20,MESFUNC6:100;
    hence |.f.| is_integrable_on M by A5,A7,A10,A1,A2,A3,A4,A11,A12,MESFUNC6:96
;
  end;
  hereby
    assume
A21: |.f.| is_integrable_on M;
    now
      let x be Element of X;
A22:  |.Im(f.x) qua Complex.| <= |.f.x.| by COMPLEX1:79;
      assume
A23:  x in dom Im f;
      then |.f.|.x = |.f.x .| by A5,A10,A4,VALUED_1:def 11;
      hence |.Im(f).x qua Complex .| <= |.f.|.x
                by A23,A22,COMSEQ_3:def 4;
    end;
    then
A24: Im f is_integrable_on M by A5,A10,A8,A4,A21,MESFUNC6:96;
    now
      let x be Element of X;
A25:  |.Re(f.x) qua Complex.| <= |.f.x .| by COMPLEX1:79;
      assume
A26:  x in dom Re f;
      then |.f.|.x = |.f.x .| by A5,A7,A4,VALUED_1:def 11;
      hence |.Re(f).x qua Complex .| <= |.f.|.x
            by A26,A25,COMSEQ_3:def 3;
    end;
    then Re f is_integrable_on M by A5,A7,A9,A4,A21,MESFUNC6:96;
    hence f is_integrable_on M by A24;
  end;
end;

theorem
  f is_integrable_on M & g is_integrable_on M implies dom (f+g) in S
proof
  assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
A3: Re g is_integrable_on M by A2;
A4: Im g is_integrable_on M by A2;
  Im f is_integrable_on M by A1;
  then dom(Im(f)+Im(g)) in S by A4,MESFUNC6:99;
  then
A5: dom(Im(f+g)) in S by Th5;
  Re f is_integrable_on M by A1;
  then dom(Re(f)+Re(g)) in S by A3,MESFUNC6:99;
  then
A6: dom(Re(f+g)) in S by Th5;
  dom(<i>(#)Im(f+g)) = dom(Im(f+g)) by VALUED_1:def 5;
  then dom(Re(f+g) + <i>(#)Im(f+g)) = dom(Re(f+g)) /\ dom(Im(f+g)) by
VALUED_1:def 1;
  then dom(Re(f+g) + <i>(#)Im(f+g)) in S by A6,A5,FINSUB_1:def 2;
  hence thesis by Th8;
end;

theorem Th33:
  f is_integrable_on M & g is_integrable_on M implies f+g is_integrable_on M
proof
  assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
A3: Im g is_integrable_on M by A2;
  Im f is_integrable_on M by A1;
  then Im(f)+ Im(g) is_integrable_on M by A3,MESFUNC6:100;
  then
A4: Im(f+g) is_integrable_on M by Th5;
A5: Re g is_integrable_on M by A2;
  Re f is_integrable_on M by A1;
  then Re(f)+ Re(g) is_integrable_on M by A5,MESFUNC6:100;
  then Re(f+g) is_integrable_on M by Th5;
  hence thesis by A4;
end;

theorem Th34:
  for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f,g be PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M
  holds f-g is_integrable_on M
proof
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g
  be PartFunc of X,REAL;
  assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
  R_EAL g is_integrable_on M by A2;
  then (-jj)(#)R_EAL g is_integrable_on M by MESFUNC5:110;
  then -R_EAL g is_integrable_on M by MESFUNC2:9;
  then
A3: R_EAL -g is_integrable_on M by MESFUNC6:28;
  R_EAL f is_integrable_on M by A1;
  then R_EAL f + R_EAL -g is_integrable_on M by A3,MESFUNC5:108;
  then R_EAL(f-g) is_integrable_on M by MESFUNC6:23;
  hence thesis;
end;

theorem
  f is_integrable_on M & g is_integrable_on M implies f-g is_integrable_on M
proof
  assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
A3: Im g is_integrable_on M by A2;
  Im f is_integrable_on M by A1;
  then Im(f)- Im(g) is_integrable_on M by A3,Th34;
  then
A4: Im(f-g) is_integrable_on M by Th6;
A5: Re g is_integrable_on M by A2;
  Re f is_integrable_on M by A1;
  then Re(f)- Re(g) is_integrable_on M by A5,Th34;
  then Re(f-g) is_integrable_on M by Th6;
  hence thesis by A4;
end;

theorem Th36:
  f is_integrable_on M & g is_integrable_on M implies ex E be
Element of S st E = dom f /\ dom g & Integral(M,f+g)=Integral(M,f|E)+Integral(M
  ,g|E)
proof
  assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
A3: Re g is_integrable_on M by A2;
  Re f is_integrable_on M by A1;
  then consider E be Element of S such that
A4: E = dom Re f /\ dom Re g and
A5: Integral(M,Re(f)+Re(g))=Integral(M,(Re f)|E)+Integral(M,(Re g)|E) by A3,
MESFUNC6:101;
A6: f|E is_integrable_on M by A1,Th23;
  then
A7: Re(f|E) is_integrable_on M;
  then
A8: Integral(M,Re(f|E)) < +infty by MESFUNC6:90;
A9: Im(f|E) is_integrable_on M by A6;
  then
A10: -infty < Integral(M,Im(f|E)) by MESFUNC6:90;
A11: Integral(M,Im(f|E)) < +infty by A9,MESFUNC6:90;
  -infty < Integral(M,Re(f|E)) by A7,MESFUNC6:90;
  then reconsider R1=Integral(M,Re(f|E)), I1=Integral(M,Im(f|E))
as Element of REAL by A8
,A10,A11,XXREAL_0:14;
A12: dom f = dom Re f by COMSEQ_3:def 3;
A13: Im g is_integrable_on M by A2;
  Im f is_integrable_on M by A1;
  then
A14: ex Ei be Element of S st Ei = dom Im f /\ dom Im g & Integral(M,Im(f)+Im
  (g))=Integral(M,Im(f)|Ei)+Integral(M,Im(g)|Ei) by A13,MESFUNC6:101;
A15: Integral(M,Im(f)+Im(g)) = Integral(M,Im(f+g)) by Th5;
A16: f+g is_integrable_on M by A1,A2,Th33;
  then
A17: Re(f+g) is_integrable_on M;
  then
A18: Integral(M,Re(f+g)) < +infty by MESFUNC6:90;
A19: Im(f+g) is_integrable_on M by A16;
  then
A20: -infty < Integral(M,Im(f+g)) by MESFUNC6:90;
A21: Integral(M,Im(f+g)) < +infty by A19,MESFUNC6:90;
  -infty < Integral(M,Re(f+g)) by A17,MESFUNC6:90;
  then reconsider R=Integral(M,Re(f+g)), I=Integral(M,Im(f+g))
as Element of REAL by A18
,A20,A21,XXREAL_0:14;
A22: Integral(M,f+g) = R + I * <i> by A16,Def3;
A23: dom g = dom Im g by COMSEQ_3:def 4;
A24: g|E is_integrable_on M by A2,Th23;
  then
A25: Re(g|E) is_integrable_on M;
  then
A26: Integral(M,Re(g|E)) < +infty by MESFUNC6:90;
A27: Im(g|E) is_integrable_on M by A24;
  then
A28: -infty < Integral(M,Im(g|E)) by MESFUNC6:90;
A29: Integral(M,Im(g|E)) < +infty by A27,MESFUNC6:90;
  -infty < Integral(M,Re(g|E)) by A25,MESFUNC6:90;
  then reconsider R2=Integral(M,Re(g|E)), I2=Integral(M,Im(g|E))
as Element of REAL by A26
,A28,A29,XXREAL_0:14;
A30: dom g = dom Re g by COMSEQ_3:def 3;
  Integral(M,Re(f)+Re(g)) = Integral(M,Re(f+g)) by Th5;
  then Integral(M,Re(f+g)) = Integral(M,Re(f|E)) + Integral(M,Re(g)|E) by A5
,Th7
    .= Integral(M,Re(f|E)) + Integral(M,Re(g|E)) by Th7;
  then
A31: R = R1 + R2 by SUPINF_2:1;
  dom f = dom Im f by COMSEQ_3:def 4;
  then Integral(M,Im(f+g)) = Integral(M,Im(f|E)) + Integral(M,Im(g)|E) by A4
,A12,A30,A23,A14,A15,Th7;
  then I = I1 + (I2 qua ExtReal) by Th7;
  then I = I1 + I2;
  then Integral(M,f+g) = (R1 + I1 * <i>) + (R2 + I2 * <i>) by A31,A22;
  then Integral(M,f+g) = Integral(M,f|E) + (R2 + I2 * <i>) by A6,Def3;
  then Integral(M,f+g) = Integral(M,f|E)+Integral(M,g|E) by A24,Def3;
  hence thesis by A4,A12,A30;
end;

theorem
  for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
  ex E be Element of S st E = dom f /\ dom g & Integral(M,f-g)=Integral(M,f|E)+
  Integral(M,(-g)|E)
proof
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g
  be PartFunc of X,REAL;
  assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
  R_EAL g is_integrable_on M by A2;
  then (-jj)(#)R_EAL g is_integrable_on M by MESFUNC5:110;
  then -R_EAL g is_integrable_on M by MESFUNC2:9;
  then
A3: R_EAL -g is_integrable_on M by MESFUNC6:28;
  R_EAL f is_integrable_on M by A1;
  then consider E be Element of S such that
A4: E = dom(R_EAL f) /\ dom(R_EAL -g) and
A5: Integral(M,R_EAL f + R_EAL -g) = Integral(M,(R_EAL f)|E) + Integral(
  M,(R_EAL -g)|E) by A3,MESFUNC5:109;
  take E;
  dom(R_EAL -g) = dom(-R_EAL g) by MESFUNC6:28;
  hence thesis by A4,A5,MESFUNC1:def 7,MESFUNC6:23;
end;

theorem Th38:
  f is_integrable_on M implies r(#)f is_integrable_on M & Integral
  (M,r(#)f) = r * Integral(M,f)
proof
A1: Integral(M,r(#)Re(f)) = Integral(M,Re(r(#)f)) by Th2;
A2: Integral(M,r(#)Im(f)) = Integral(M,Im(r(#)f)) by Th2;
  assume
A3: f is_integrable_on M;
  then
A4: Re f is_integrable_on M;
  then
A5: Integral(M,Re f) < +infty by MESFUNC6:90;
  r(#)Re(f) is_integrable_on M by A4,MESFUNC6:102;
  then
A6: Re(r(#)f) is_integrable_on M by Th2;
  then
A7: Integral(M,Re(r(#)f)) < +infty by MESFUNC6:90;
A8: Im f is_integrable_on M by A3;
  then
A9: -infty < Integral(M,Im f) by MESFUNC6:90;
A10: Integral(M,Im f) < +infty by A8,MESFUNC6:90;
  -infty < Integral(M,Re f) by A4,MESFUNC6:90;
  then reconsider R1=Integral(M,Re f), I1=Integral(M,Im f)
as Element of REAL by A5,A9,A10
,XXREAL_0:14;
A11: (r qua ExtReal) * R1 = r * R1;
A12: (r qua ExtReal) * I1 = r * I1;
  r(#)Im(f) is_integrable_on M by A8,MESFUNC6:102;
  then
A13: Im(r(#)f) is_integrable_on M by Th2;
  then
A14: -infty < Integral(M,Im(r(#)f)) by MESFUNC6:90;
A15: Integral(M,Im(r(#)f)) < +infty by A13,MESFUNC6:90;
  -infty < Integral(M,Re(r(#)f)) by A6,MESFUNC6:90;
  then reconsider
  R2=Integral(M,Re(r(#)f)), I2=Integral(M,Im(r(#)f))
as Element of REAL by A7,A14,A15,
XXREAL_0:14;
A16: Integral(M,r(#)Im(f)) =  r * Integral(M,Im f) by A8,MESFUNC6:102;
A17: r(#)f is_integrable_on M by A6,A13;
  Integral(M,r(#)Re(f))
    = (r qua ExtReal) * Integral(M,Re f) by A4,MESFUNC6:102;
  then R2 + I2 * <i> = r * (R1 + I1 * <i>) by A16,A1,A2,A11,A12;
  then Integral(M,r(#)f) = r * (R1 + I1 * <i>) by A17,Def3;
  hence thesis by A3,A6,A13,Def3;
end;

theorem Th39:
  f is_integrable_on M implies <i>(#)f is_integrable_on M &
  Integral(M,<i>(#)f) = <i> * Integral(M,f)
proof
A1: Re(<i>(#)f) = -Im(f) by Th4;
  assume
A2: f is_integrable_on M;
  then
A3: Im f is_integrable_on M;
A4: Im(<i>(#)f)= Re f by Th4;
  then
A5: Im(<i>(#)f) is_integrable_on M by A2;
  Re(<i>(#)f) is_integrable_on M by A3,A1,MESFUNC6:102;
  hence <i>(#)f is_integrable_on M by A5;
  then consider R1,I1 be Real such that
A6: R1=Integral(M,Re(<i>(#)f)) and
A7: I1 =Integral(M,Im(<i>(#)f)) and
A8: Integral(M,<i>(#)f)=R1+ I1 * <i> by Def3;
  consider R,I be Real such that
A9: R=Integral(M,Re f) and
A10: I =Integral(M,Im f) and
A11: Integral(M,f)=R+ I * <i> by A2,Def3;
  R1 = (-1) * (I qua ExtReal) by A3,A1,A10,A6,MESFUNC6:102
    .=(-1)*I;
  hence thesis by A4,A9,A11,A7,A8;
end;

theorem Th40:
  f is_integrable_on M implies c(#)f is_integrable_on M & Integral
  (M,c(#)f) = c * Integral(M,f)
proof
A1: c = Re(c) + Im(c) * <i> by COMPLEX1:13;
A2: dom(<i>(#)f) = dom f by VALUED_1:def 5;
  assume
A3: f is_integrable_on M;
  then
A4: Integral(M,(Re c)(#)f) = Re c * Integral(M,f) by Th38;
A5: <i>(#)f is_integrable_on M by A3,Th39;
  then
A6: (Im c)(#)(<i>(#)f) is_integrable_on M by Th38;
A7: (Re c)(#)f is_integrable_on M by A3,Th38;
  then consider E be Element of S such that
A8: E = dom ((Re c)(#)f) /\ dom ((Im c)(#)(<i>(#)f)) and
A9: Integral(M,(Re c)(#)f + (Im c)(#)(<i>(#)f)) = Integral(M,((Re c)(#)
  f)|E) + Integral(M,((Im c)(#)(<i>(#)f))|E) by A6,Th36;
A10: dom(c(#)f) = dom f by VALUED_1:def 5;
A11: Integral(M,(Im c)(#)(<i>(#)f)) = Im c * Integral(M,<i>(#)f) by A5,Th38;
A12: dom(Re(c)(#)f) = dom f by VALUED_1:def 5;
A13: dom((Im c)(#)(<i>(#)f)) = dom(<i>(#)f) by VALUED_1:def 5;
A14: dom((Re c)(#)f + (Im c)(#)(<i>(#)f)) = dom((Re c)(#)f) /\ dom((Im c)(#)(
  <i>(#)f)) by VALUED_1:def 1;
  now
    let x be Element of X;
    assume
A15: x in dom(c(#)f);
    then
A16: (c(#)f).x = c * f.x by VALUED_1:def 5;
A17: ((Im c)(#)(<i>(#)f)).x = Im c * (<i>(#)f).x by A10,A2,A13,A15,
VALUED_1:def 5;
A18: ((Re c)(#)f).x= Re c * f.x by A10,A12,A15,VALUED_1:def 5;
A19: (<i>(#)f).x = <i> * f.x by A10,A2,A15,VALUED_1:def 5;
    ((Re c)(#)f + (Im c)(#)(<i>(#)f)).x = ((Re c)(#)f).x + ((Im c)(#)(<i>
    (#) f)).x by A10,A12,A2,A13,A14,A15,VALUED_1:def 1;
    hence (c(#)f).x = ((Re c)(#)f + (Im c)(#)(<i>(#)f)).x by A1,A16,A18,A17,A19
;
  end;
  then
A20: c(#)f = (Re c)(#)f + (Im c)(#)(<i>(#)f) by A10,A12,A2,A13,A14,PARTFUN1:5;
  hence c(#)f is_integrable_on M by A7,A6,Th33;
A21: Integral(M,<i>(#)f) = <i> * Integral(M,f) by A3,Th39;
  thus
  Integral(M,c(#)f) = Re c * Integral(M,f) + (Im c)*<i>* Integral(M,f) by A12
,A2,A13,A20,A4,A21,A11,A8,A9
    .= c * Integral(M,f) by A1;
end;

Lm2: ( ex A be Element of S st A = dom f & f is A-measurable ) & f
is_integrable_on M & Integral(M,f) = 0 implies |. Integral(M,f).| <= Integral(M
,|.f.|)
proof
  assume that
A1: ex A be Element of S st A = dom f & f is A-measurable and
A2: f is_integrable_on M and
A3: Integral(M,f) = 0;
A4: |.f.| is_integrable_on M by A1,A2,Th31;
  consider R,I be Real such that
A5: R = Integral(M,Re f) and
  I = Integral(M,Im f) and
A6: Integral(M,f)=R + I * <i> by A2,Def3;
  R = 0 by A3,A6,COMPLEX1:4,12;
  then
A7: |.Integral(M,Re f).| = 0 by A5,EXTREAL1:16;
  Re f is_integrable_on M by A2;
  then
A8: |.Integral(M,Re f).| <= Integral(M,|.Re f.|) by MESFUNC6:95;
A9: dom |.f.| = dom f by VALUED_1:def 11;
  consider A be Element of S such that
A10: A = dom f and
A11: f is A-measurable by A1;
A12: dom Re f = A by A10,COMSEQ_3:def 3;
A13: now
    let x be Element of X;
    assume
A14: x in dom Re f;
    then
A15: Re(f).x = Re(f.x) by COMSEQ_3:def 3;
    |.f.|.x = |.f.x .| by A10,A12,A9,A14,VALUED_1:def 11;
    hence |.Re(f).x qua Complex .| <= |.f.|.x by A15,COMPLEX1:79;
  end;
  Re f is A-measurable by A11;
  hence thesis by A3,A4,A8,A10,A12,A9,A13,A7,COMPLEX1:44,MESFUNC6:96;
end;

theorem Th41:
  for f be PartFunc of X,REAL,Y,r holds (r(#)f)|Y = r(#)(f|Y)
proof
  let f be PartFunc of X,REAL,Y,r;
A1: dom ((r(#)f)|Y) = dom (r(#)f) /\ Y by RELAT_1:61
    .= dom f /\ Y by VALUED_1:def 5
    .= dom (f|Y) by RELAT_1:61;
A2: dom((r(#)f)|Y) c= dom (r(#)f) by RELAT_1:60;
A3: now
    let x be Element of X;
    assume
A4: x in dom((r(#)f)|Y);
    then x in dom (r(#)(f|Y)) by A1,VALUED_1:def 5;
    then (r(#)(f|Y)).x = r*((f|Y).x) by VALUED_1:def 5;
    then (r(#)(f|Y)).x = r*((f.x)) by A1,A4,FUNCT_1:47;
    then (r(#)(f|Y)).x = (r(#)f).x by A2,A4,VALUED_1:def 5;
    hence (r(#)(f|Y)).x = ((r(#)f)|Y).x by A4,FUNCT_1:47;
  end;
  dom ((r(#)f)|Y) = dom (r(#)(f|Y)) by A1,VALUED_1:def 5;
  hence thesis by A3,PARTFUN1:5;
end;

theorem Th42:
  for f,g be PartFunc of X,REAL st ( ex A be Element of S st A =
  dom f /\ dom g & f is A-measurable & g is A-measurable ) & f
  is_integrable_on M & g is_integrable_on M & g-f is nonnegative holds ex E be
  Element of S st E = dom f /\ dom g & Integral(M,f|E) <= Integral(M,g|E)
proof
  let f,g be PartFunc of X,REAL;
  assume that
A1: ex A be Element of S st A = dom f /\ dom g & f is A-measurable &
  g is A-measurable and
A2: f is_integrable_on M and
A3: g is_integrable_on M and
A4: g-f is nonnegative;
  set h=(-1)(#)f;
  h is_integrable_on M by A2,MESFUNC6:102;
  then consider E be Element of S such that
A5: E = dom h /\ dom g and
A6: Integral(M,h+g) = Integral(M,h|E)+Integral(M,g|E) by A3,MESFUNC6:101;
A7: f|E is_integrable_on M by A2,MESFUNC6:91;
  then
A8: Integral(M,f|E) < +infty by MESFUNC6:90;
  -infty < Integral(M,f|E) by A7,MESFUNC6:90;
  then reconsider c1=Integral(M,f|E) as Element of REAL by A8,XXREAL_0:14;
A9: (-1) * Integral(M,f|E) = (-1)*c1 by EXTREAL1:1;
A10: g|E is_integrable_on M by A3,MESFUNC6:91;
  then
A11: Integral(M,g|E) < +infty by MESFUNC6:90;
  -infty < Integral(M,g|E) by A10,MESFUNC6:90;
  then reconsider c2=Integral(M,g|E) as Element of REAL by A11,XXREAL_0:14;
  take E;
A12: h|E = (-1)(#)(f|E) by Th41;
  consider A be Element of S such that
A13: A = dom f /\ dom g and
A14: f is A-measurable and
A15: g is A-measurable by A1;
  dom h = dom f by VALUED_1:def 5;
  then
A16: dom(h+g) = A by A13,VALUED_1:def 1;
  h is A-measurable by A13,A14,MESFUNC6:21,XBOOLE_1:17;
  then 0 <= Integral(M,h|E)+Integral(M,g|E) by A4,A6,A15,A16,MESFUNC6:26,84;
  then 0 <= (-1) * Integral(M,f|E) + Integral(M,g|E) by A7,A12,
MESFUNC6:102;
  then 0 <= -c1 + c2 by A9,SUPINF_2:1;
  then (0 qua Real) +c1 <= -c1+c2+c1 by XREAL_1:6;
  hence thesis by A5,VALUED_1:def 5;
end;

Lm3: ( ex A be Element of S st A = dom f & f is A-measurable ) & f
is_integrable_on M & Integral(M,f) <> 0 implies |. Integral(M,f).| <= Integral(
M,|.f.|)
proof
  assume that
A1: ex A be Element of S st A = dom f & f is A-measurable and
A2: f is_integrable_on M and
A3: Integral(M,f) <> 0;
A4: |.f.| is_integrable_on M by A1,A2,Th31;
  set a = Integral(M,f);
  0 < |.a.| by A3,COMPLEX1:47;
  then
A5: |.a.|/|.a.| = 1 by XCMPLX_1:60;
  set h = f (#) (|.f.|");
  set b = a / |.a.|;
A6: dom |.f.| = dom f by VALUED_1:def 11;
  |.b.|*|.b*'.| = |.b*b*'.| by COMPLEX1:65;
  then |.b.|*|.b*'.| = |.b*b.| by COMPLEX1:69;
  then
A7: |.b.|*|.b*'.| = |.a / |.a.|.|*|.a / |.a.|.| by COMPLEX1:65;
A8: h = f /" |.f.|;
  then
A9: dom h = dom f /\ dom |.f.| by VALUED_1:16;
  then
A10: dom(b*'(#)h) = dom f by A6,VALUED_1:def 5;
  then
A11: dom(|.f.|(#)(b*'(#)h)) = dom f /\ dom f by A6,VALUED_1:def 4;
  then
A12: dom(Re(|.f.|(#)(b*'(#)h))) = dom f by COMSEQ_3:def 3;
A13: dom(|.f.|(#)h) = dom|.f.| /\ dom h by VALUED_1:def 4;
  then
A14: dom(b*'(#)(|.f.|(#)h)) = dom f by A6,A9,VALUED_1:def 5;
  now
    let x be object;
    assume
A15: x in dom(b*'(#)(|.f.|(#)h));
    then x in dom(|.f.|(#)(b*'(#)h)) by A6,A9,A13,A11,VALUED_1:def 5;
    then (|.f.|(#)(b*'(#)h)).x = (|.f.|.x)*((b*'(#)h).x) by VALUED_1:def 4;
    then (|.f.|(#)(b*'(#)h)).x = |.f.x .|*((b*'(#)h).x) by A6,A14,A15,
VALUED_1:def 11;
    then
A16: (|.f.|(#)(b*'(#)h)).x = (b*'*(h.x))*|.f.x .| by A14,A10,A15,VALUED_1:def 5
;
    (b*'(#)(|.f.|(#)h)).x = b*'*((|.f.|(#)h).x) by A15,VALUED_1:def 5;
    then
    (b*'(#)(|.f.|(#)h)).x = b*'*((|.f.|.x)*(h.x)) by A6,A9,A13,A14,A15,
VALUED_1:def 4;
    then (b*'(#)(|.f.|(#)h)).x = b*'*(|.f.x .|*(h.x)) by A6,A14,A15,
VALUED_1:def 11;
    hence (b*'(#)(|.f.|(#)h)).x = (|.f.|(#)(b*'(#)h)).x by A16;
  end;
  then
A17: b*'(#)(|.f.|(#)h) = |.f.|(#)(b*'(#)h) by A14,A11,FUNCT_1:2;
A18: |.a / |.a qua Complex.| qua Complex.|
     = |.a.|/|.|.a qua Complex.| qua Complex.|
         by COMPLEX1:67;
  now
    let x be set;
A19: h.x = f.x / |.f.|.x by A8,VALUED_1:17;
    assume
A20: x in dom(Re(|.f.|(#)(b*'(#)h))) /\ dom |.f.|;
    then |.f.|.x = |.f.x .| by A6,A12,VALUED_1:def 11;
    then
A21: |.h.x .| = |.f.x .| / |.|.f.x .| qua Complex.| by A19,COMPLEX1:67;
    per cases;
    suppose
A22:  f.x <> 0;
A23:  Re((|.f.|(#)(b*'(#)h)).x) = Re(|.f.|(#)(b*'(#)h)).x by A6,A12,A20,
COMSEQ_3:def 3;
      (|.f.|(#)(b*'(#)h)).x = (|.f.|.x)*((b*'(#)h).x) by A6,A11,A12,A20,
VALUED_1:def 4;
      then (|.f.|(#)(b*'(#)h)).x = |.f.x .|*((b*'(#)h).x) by A6,A12,A20,
VALUED_1:def 11;
      then
A24:  |.(|.f.|(#)(b*'(#)h)).x qua Complex .|
         = |.|.f.x .| qua Complex.|*|.(b*'(#)h).x qua Complex .|
          by COMPLEX1:65;
      x in dom(b*'(#)h) by A9,A12,A20,VALUED_1:def 5;
      then (b*'(#)h).x = b*'*(h.x) by VALUED_1:def 5;
      then
A25:  |.(b*'(#)h).x .| = |.b*'.|*|.h.x .| by COMPLEX1:65;
      0 < |.f.x .| by A22,COMPLEX1:47;
      then |.f.x .| / |.f.x .| = 1 by XCMPLX_1:60;
      then Re((|.f.|(#)(b*'(#)h)).x) <= |.f.x .|
      by A7,A18,A5,A21,A25,A24,
COMPLEX1:54;
      hence Re(|.f.|(#)(b*'(#)h)).x <= |.f.|.x by A6,A12,A20,A23,
VALUED_1:def 11;
    end;
    suppose
A26:  f.x = 0;
      (|.f.|(#)(b*'(#)h)).x = (|.f.|.x)*((b*'(#)h).x) by A6,A11,A12,A20,
VALUED_1:def 4;
      then (|.f.|(#)(b*'(#)h)).x = |.f.x .|*((b*'(#)h).x) by A6,A12,A20,
VALUED_1:def 11;
      then
A27:  |.(|.f.|(#)(b*'(#)h)).x qua Complex .|
        = |.|.f.x qua Complex .| qua Complex.|*|.(b*'(#)h).x qua Complex .|
      by COMPLEX1:65;
      (Re(f.x))^2 + (Im(f.x))^2 = 0 by A26,COMPLEX1:5;
      then
A28:  Re((|.f.|(#)(b*'(#)h)).x) <= |.f.x qua Complex .|
           by A27,COMPLEX1:54,SQUARE_1:17;
      Re((|.f.|(#)(b*'(#)h)).x) = Re(|.f.|(#)(b*'(#)h)).x by A6,A12,A20,
COMSEQ_3:def 3;
      hence Re(|.f.|(#)(b*'(#)h)).x <= |.f.|.x by A6,A12,A20,A28,
VALUED_1:def 11;
    end;
  end;
  then
A29: |.f.| - Re(|.f.|(#)(b*'(#)h)) is nonnegative by MESFUNC6:58;
  set F = Re(|.f.|(#)(b*'(#)h));
  reconsider b1=b as Element of COMPLEX by XCMPLX_0:def 2;
A30: Re(b1*b1*') = (Re b1)^2 + (Im b1)^2 by COMPLEX1:40;
  consider A be Element of S such that
A31: A = dom f and
A32: f is A-measurable by A1;
A33: |.f.| is A-measurable by A31,A32,Th30;
A34: now
    let x be object;
A35: h.x = (f.x)/|.f.|.x by A8,VALUED_1:17;
    assume
A36: x in dom f;
    then
A37: |.f.|.x = |.f.x .| by A6,VALUED_1:def 11;
A38: (|.f.|(#)h).x = (|.f.|.x)*(h.x) by A6,A9,A13,A36,VALUED_1:def 4;
    per cases;
    suppose
      f.x <> 0;
      then 0 < |.f.x .| by COMPLEX1:47;
      hence f.x = (|.f.|(#)h).x by A38,A37,A35,XCMPLX_1:87;
    end;
    suppose
A39:  f.x = 0;
      then (Re(f.x))^2 + (Im(f.x))^2 = 0 by COMPLEX1:5;
      then f.x = (h.x)*|.f.x .| by A39,SQUARE_1:17;
      hence f.x = (|.f.|(#)h).x by A6,A36,A38,VALUED_1:def 11;
    end;
  end;
  then
A40: f = |.f.| (#) h by A6,A9,A13,FUNCT_1:2;
  then
A41: b*'(#)(|.f.|(#)h) is_integrable_on M by A2,Th40;
  then consider R1,I1 be Real such that
A42: R1 = Integral(M,Re(|.f.|(#)(b*'(#)h))) and
  I1 = Integral(M,Im(|.f.|(#)(b*'(#)h))) and
A43: Integral(M,|.f.|(#)(b*'(#)h)) = R1 + I1 * <i> by A17,Def3;
A44: Im(b1*b1*') = 0 by COMPLEX1:40;
  reconsider aa = |.a.| as Element of REAL by XREAL_0:def 1;
  b*b*' = Re(b*b*') + (Im(b*b*'))*<i> by COMPLEX1:13;
  then b*b*' = |.b*b qua Complex.| by A30,A44,COMPLEX1:68;
  then (b*' * a) / |.a qua Complex.| = 1 by A7,A18,A5,COMPLEX1:65;
  then
A45: b*' * a = |.a.| by XCMPLX_1:58;
  Re(R1 + I1 * <i>) = R1 by COMPLEX1:12;
  then Re |.aa qua Complex.| = R1 by A2,A45,A40,A17,A43,Th40;
  then
A46: |.aa qua Complex.| = Integral(M,Re(|.f.|(#)(b*'(#)h)))
          by A42,COMPLEX1:def 1;
  |.f.| (#) h is A-measurable by A32,A6,A9,A13,A34,FUNCT_1:2;
  then b*'(#)(|.f.|(#)h) is A-measurable by A31,A6,A9,A13,Th17;
  then
A47: Re(|.f.|(#)(b*'(#)h)) is A-measurable by A17;
  Re(|.f.|(#)(b*'(#)h)) is_integrable_on M by A17,A41;
  then consider E be Element of S such that
A48: E = dom F /\ dom |.f.| and
A49: Integral(M,F|E) <= Integral(M,|.f.||E) by A4,A31,A6,A33,A47,A12,A29,Th42;
  thus thesis by A6,A46,A12,A48,A49;
end;

theorem
  ( ex A be Element of S st A = dom f & f is A-measurable ) & f
  is_integrable_on M implies |. Integral(M,f).| <= Integral(M,|.f.|)
proof
  assume that
A1: ex A be Element of S st A = dom f & f is A-measurable and
A2: f is_integrable_on M;
  per cases;
  suppose
    Integral(M,f) = 0;
    hence thesis by A1,A2,Lm2;
  end;
  suppose
    Integral(M,f) <> 0;
    hence thesis by A1,A2,Lm3;
  end;
end;

definition
  let X be non empty set;
  let S be SigmaField of X;
  let M be sigma_Measure of S;
  let f be PartFunc of X,COMPLEX;
  let B be Element of S;
  func Integral_on(M,B,f) -> Complex equals
  Integral(M,f|B);
  coherence;
end;

theorem
  f is_integrable_on M & g is_integrable_on M & B c= dom(f+g) implies f+
g is_integrable_on M & Integral_on(M,B,f+g) = Integral_on(M,B,f) + Integral_on(
  M,B,g)
proof
  assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M and
A3: B c= dom(f+g);
A4: Re f is_integrable_on M by A1;
  then Re(f)|B is_integrable_on M by MESFUNC6:91;
  then
A5: Re(f|B) is_integrable_on M by Th7;
  then
A6: Integral(M,Re(f|B)) < +infty by MESFUNC6:90;
A7: Im f is_integrable_on M by A1;
  then Im(f)|B is_integrable_on M by MESFUNC6:91;
  then
A8: Im(f|B) is_integrable_on M by Th7;
  then
A9: -infty < Integral(M,Im(f|B)) by MESFUNC6:90;
A10: Integral(M,Im(f|B)) < +infty by A8,MESFUNC6:90;
  -infty < Integral(M,Re(f|B)) by A5,MESFUNC6:90;
  then reconsider R1=Integral(M,Re(f|B)), I1=Integral(M,Im(f|B))
as Element of REAL by A6
,A9,A10,XXREAL_0:14;
  f|B is_integrable_on M by A5,A8;
  then
A11: Integral(M,f|B) = R1 + I1*<i> by Def3;
A12: Im g is_integrable_on M by A2;
  then Im(g)|B is_integrable_on M by MESFUNC6:91;
  then
A13: Im(g|B) is_integrable_on M by Th7;
  then
A14: -infty < Integral(M,Im(g|B)) by MESFUNC6:90;
A15: Re g is_integrable_on M by A2;
  then Re(g)|B is_integrable_on M by MESFUNC6:91;
  then
A16: Re(g|B) is_integrable_on M by Th7;
  then
A17: Integral(M,Re(g|B)) < +infty by MESFUNC6:90;
  B c= dom Im(f+g) by A3,COMSEQ_3:def 4;
  then
A18: B c= dom(Im(f)+Im(g)) by Th5;
  then
  Integral_on(M,B,Im(f)+Im(g)) = Integral_on(M,B,Im f) + Integral_on(M,B,
  Im g) by A7,A12,MESFUNC6:103;
  then
A19: Integral(M,Im(f+g)|B) = Integral(M,Im(f)|B) + Integral(M,Im(g)|B) by Th5;
A20: Integral(M,Im(g|B)) < +infty by A13,MESFUNC6:90;
  -infty < Integral(M,Re(g|B)) by A16,MESFUNC6:90;
  then reconsider R2=Integral(M,Re(g|B)), I2=Integral(M,Im(g|B))
as Element of REAL by A17
,A14,A20,XXREAL_0:14;
  g|B is_integrable_on M by A16,A13;
  then
A21: Integral(M,g|B) = R2 + I2*<i> by Def3;
A22: Integral(M,Im(g)|B) = I2 by Th7;
  Im(f)+Im(g) is_integrable_on M by A7,A12,A18,MESFUNC6:103;
  then
A23: Im(f+g) is_integrable_on M by Th5;
  then Im(f+g)|B is_integrable_on M by MESFUNC6:91;
  then
A24: Im((f+g)|B) is_integrable_on M by Th7;
  then
A25: -infty < Integral(M,Im((f+g)|B)) by MESFUNC6:90;
  B c= dom Re(f+g) by A3,COMSEQ_3:def 3;
  then
A26: B c= dom(Re(f)+Re(g)) by Th5;
  then
  Integral_on(M,B,Re(f)+Re(g)) = Integral_on(M,B,Re f) + Integral_on(M,B,
  Re g) by A4,A15,MESFUNC6:103;
  then
A27: Integral(M,Re(f+g)|B) = Integral(M,Re(f)|B) + Integral(M,Re(g)|B) by Th5;
  Re(f)+Re(g) is_integrable_on M by A4,A15,A26,MESFUNC6:103;
  then
A28: Re(f+g) is_integrable_on M by Th5;
  then Re(f+g)|B is_integrable_on M by MESFUNC6:91;
  then
A29: Re((f+g)|B) is_integrable_on M by Th7;
  then
A30: Integral(M,Re((f+g)|B)) < +infty by MESFUNC6:90;
A31: Integral(M,Im((f+g)|B)) < +infty by A24,MESFUNC6:90;
  -infty < Integral(M,Re((f+g)|B)) by A29,MESFUNC6:90;
  then reconsider
  R=Integral(M,Re((f+g)|B)), I=Integral(M,Im((f+g)|B))
as Element of REAL by A30,A25,A31,
XXREAL_0:14;
A32: Integral(M,Re(g)|B) = R2 by Th7;
  Integral(M,Im(f)|B) = I1 by Th7;
  then I = I1 + (I2 qua ExtReal) by A19,A22,Th7;
  then
A33: I = I1 + I2;
  Integral(M,Re(f)|B) = R1 by Th7;
  then R = R1 + (R2 qua ExtReal) by A27,A32,Th7;
  then
A34: R = R1 + R2;
  (f+g)|B is_integrable_on M by A29,A24;
  then Integral_on(M,B,f+g) = R + I * <i> by Def3
    .= Integral_on(M,B,f) + Integral_on(M,B,g) by A34,A33,A11,A21;
  hence thesis by A28,A23;
end;

theorem
  f is_integrable_on M implies Integral_on(M,B,c(#)f) = c * Integral_on( M,B,f)
proof
  assume f is_integrable_on M;
  then
A1: f|B is_integrable_on M by Th23;
A2: dom((c(#)f)|B) = dom(c(#)f) /\ B by RELAT_1:61;
  then dom((c(#)f)|B) = dom f /\ B by VALUED_1:def 5;
  then
A3: dom((c(#)f)|B) = dom(f|B) by RELAT_1:61;
A4: now
    let x be object;
    assume
A5: x in dom((c(#)f)|B);
    then
A6: (c(#)f)|B.x= (c(#)f).x by FUNCT_1:47;
    x in dom (c(#)f) by A2,A5,XBOOLE_0:def 4;
    then (c(#)f)|B.x= c * f.x by A6,VALUED_1:def 5;
    then
A7: (c(#)f)|B.x= c * f|B.x by A3,A5,FUNCT_1:47;
    x in dom (c(#)(f|B)) by A3,A5,VALUED_1:def 5;
    hence (c(#)f)|B.x= (c(#)(f|B)).x by A7,VALUED_1:def 5;
  end;
  dom((c(#)f)|B) = dom(c(#)(f|B)) by A3,VALUED_1:def 5;
  then (c(#)f)|B = c(#)(f|B) by A4,FUNCT_1:2;
  hence thesis by A1,Th40;
end;

begin :: Several Properties of Real-valued Measurable Functions

reserve f for PartFunc of X,REAL,
  a for Real;

theorem
  for f be PartFunc of X,REAL, a be Real st A c= dom f holds A /\
  great_eq_dom(f,a) = A\(A /\ less_dom(f,a))
proof
  let f be PartFunc of X,REAL, a be Real;
  now
    let x be object;
    assume
A1: x in A /\ great_eq_dom(f,a);
    then x in great_eq_dom(f,a) by XBOOLE_0:def 4;
    then ex y be Real st y = f.x & a <= y by MESFUNC6:6;
    then not (ex y1 be Real st y1 = f.x & y1 < a);
    then not x in less_dom(f,a) by MESFUNC6:3;
    then
A2: not x in (A /\ less_dom(f,a)) by XBOOLE_0:def 4;
    x in A by A1,XBOOLE_0:def 4;
    hence x in A\(A /\ less_dom(f,a)) by A2,XBOOLE_0:def 5;
  end;
  then
A3: A /\ great_eq_dom(f,a) c= A\(A /\ less_dom(f,a)) by TARSKI:def 3;
  assume
A4: A c= dom f;
  now
    let x be object;
    assume
A5: x in A\(A /\ less_dom(f,a));
    then
A6: x in A by XBOOLE_0:def 5;
    not x in A /\ less_dom(f,a) by A5,XBOOLE_0:def 5;
    then not x in less_dom(f,a) by A6,XBOOLE_0:def 4;
    then not f.x < a by A4,A6,MESFUNC6:3;
    then x in great_eq_dom(f,a) by A4,A6,MESFUNC6:6;
    hence x in A /\ great_eq_dom(f,a) by A6,XBOOLE_0:def 4;
  end;
  then A\(A /\ less_dom(f,a)) c= A /\ great_eq_dom(f,a) by TARSKI:def 3;
  hence thesis by A3,XBOOLE_0:def 10;
end;

theorem
  for f be PartFunc of X,REAL, a be Real st A c= dom f holds A /\
  great_dom(f,a) = A\(A /\ less_eq_dom(f,a))
proof
  let f be PartFunc of X,REAL, a be Real;
  now
    let x be object;
    assume
A1: x in A /\ great_dom(f,a);
    then x in great_dom(f,a) by XBOOLE_0:def 4;
    then ex y be Real st y = f.x & a < y by MESFUNC6:5;
    then not (ex y1 be Real st y1 = f.x & y1 <= a);
    then not x in less_eq_dom(f,a) by MESFUNC6:4;
    then
A2: not x in (A /\ less_eq_dom(f,a)) by XBOOLE_0:def 4;
    x in A by A1,XBOOLE_0:def 4;
    hence x in A\(A /\ less_eq_dom(f,a)) by A2,XBOOLE_0:def 5;
  end;
  then
A3: A /\ great_dom(f,a) c= A\(A /\ less_eq_dom(f,a)) by TARSKI:def 3;
  assume
A4: A c= dom f;
  now
    let x be object;
    assume
A5: x in A\(A /\ less_eq_dom(f,a));
    then
A6: x in A by XBOOLE_0:def 5;
    not x in A /\ less_eq_dom(f,a) by A5,XBOOLE_0:def 5;
    then not x in less_eq_dom(f,a) by A6,XBOOLE_0:def 4;
    then not f.x <= a by A4,A6,MESFUNC6:4;
    then x in great_dom(f,a) by A4,A6,MESFUNC6:5;
    hence x in A /\ great_dom(f,a) by A6,XBOOLE_0:def 4;
  end;
  then A\(A /\ less_eq_dom(f,a)) c= A /\ great_dom(f,a) by TARSKI:def 3;
  hence thesis by A3,XBOOLE_0:def 10;
end;

theorem
  for f be PartFunc of X,REAL, a be Real st A c= dom f holds A /\
  less_eq_dom(f,a) = A\(A /\ great_dom(f,a))
proof
  let f be PartFunc of X,REAL, a be Real;
  now
    let x be object;
    assume
A1: x in A /\ less_eq_dom(f,a);
    then x in less_eq_dom(f,a) by XBOOLE_0:def 4;
    then ex y be Real st y = f.x & y <= a by MESFUNC6:4;
    then not (ex y1 be Real st y1 = f.x & a < y1);
    then not x in great_dom(f,a) by MESFUNC6:5;
    then
A2: not x in (A /\ great_dom(f,a)) by XBOOLE_0:def 4;
    x in A by A1,XBOOLE_0:def 4;
    hence x in A\(A /\ great_dom(f,a)) by A2,XBOOLE_0:def 5;
  end;
  then
A3: A /\ less_eq_dom(f,a) c= A\(A /\ great_dom(f,a)) by TARSKI:def 3;
  assume
A4: A c= dom f;
  now
    let x be object;
    assume
A5: x in A\(A /\ great_dom(f,a));
    then
A6: x in A by XBOOLE_0:def 5;
    not x in A /\ great_dom(f,a) by A5,XBOOLE_0:def 5;
    then not x in great_dom(f,a) by A6,XBOOLE_0:def 4;
    then not a < f.x by A4,A6,MESFUNC6:5;
    then x in less_eq_dom(f,a) by A4,A6,MESFUNC6:4;
    hence x in A /\ less_eq_dom(f,a) by A6,XBOOLE_0:def 4;
  end;
  then A\(A /\ great_dom(f,a)) c= A /\ less_eq_dom(f,a) by TARSKI:def 3;
  hence thesis by A3,XBOOLE_0:def 10;
end;

theorem
  A /\ eq_dom(f,a) = A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a)
proof
  now
    let x be object;
    assume
A1: x in A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a);
    then
A2: x in less_eq_dom(f,a) by XBOOLE_0:def 4;
    then
A3: x in dom f by MESFUNC6:4;
A4: x in A /\ great_eq_dom(f,a) by A1,XBOOLE_0:def 4;
    then x in great_eq_dom(f,a) by XBOOLE_0:def 4;
    then
A5: ex y1 be Real st y1 = f.x & a <= y1 by MESFUNC6:6;
    ex y2 be Real st y2 = f.x & y2 <= a by A2,MESFUNC6:4;
    then a = f.x by A5,XXREAL_0:1;
    then
A6: x in eq_dom(f,a) by A3,MESFUNC6:7;
    x in A by A4,XBOOLE_0:def 4;
    hence x in A /\ eq_dom(f,a) by A6,XBOOLE_0:def 4;
  end;
  then
A7: A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a) c= A /\ eq_dom(f,a) by
TARSKI:def 3;
  now
    let x be object;
    assume
A8: x in A /\ eq_dom(f,a);
    then
A9: x in A by XBOOLE_0:def 4;
A10: x in eq_dom(f,a) by A8,XBOOLE_0:def 4;
    then
A11: ex y be Real st y = f.x & a = y by MESFUNC6:7;
A12: x in dom f by A10,MESFUNC6:7;
    then x in great_eq_dom(f,a) by A11,MESFUNC6:6;
    then
A13: x in A /\ great_eq_dom(f,a) by A9,XBOOLE_0:def 4;
    x in less_eq_dom(f,a) by A11,A12,MESFUNC6:4;
    hence x in A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a) by A13,XBOOLE_0:def 4
;
  end;
  then A /\ eq_dom(f,a) c= A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a) by
TARSKI:def 3;
  hence thesis by A7,XBOOLE_0:def 10;
end;