:: On $L^1$ Space Formed by Real-valued Partial Functions
::  by Yasushige Watase , Noboru Endou and Yasunari Shidama
::
:: Received August 26, 2008
:: Copyright (c) 2008 Association of Mizar Users

environ

 vocabularies FUNCT_1, COMPLEX1, RELAT_1, BOOLE, PARTFUN1, SEQ_1, ARYTM_1,
      ARYTM, SQUARE_1, ARYTM_3, ABSVALUE, INTEGRA1, RLVECT_1, SUPINF_2,
      RSSPACE, STRUCT_0, ALGSTR_0, VECTSP10, REALSET1, FUNCOP_1, PRE_TOPC,
      LPSPACE1, BINOP_1, NORMSP_1, PROB_1, RLSUB_1, SUPINF_1, MEASURE1,
      MEASURE6, MESFUNC1, TARSKI, RFUNCT_3, MESFUNC2, SETFAM_1, MESFUNC5,
      IDEAL_1, SUBSET_1, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, NUMBERS, COMPLEX1,
      XXREAL_0, SUPINF_1, SUPINF_2, EXTREAL1, REALSET1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, VALUED_1, RFUNCT_3, BINOP_1, FUNCOP_1, REAL_1,
      STRUCT_0, ALGSTR_0, RLVECT_1, RLSUB_1, IDEAL_1, SETFAM_1, DOMAIN_1,
      PRE_TOPC, NORMSP_1, PROB_1, MEASURE1, MEASURE2, MEASURE3, MEASURE6,
      MESFUNC1, MESFUNC2, MESFUNC5, MESFUNC6, :::MESFUNC7,
      FUNCT_7;
 constructors COMPLEX1, EXTREAL1, NAT_1, BINOP_1, REAL_1, RLSUB_1, IDEAL_1,
      NORMSP_1, MEASURE3, MEASURE6, MESFUNC2, MESFUNC5, MESFUNC6, MESFUNC7,
      SEQ_1, MESFUNC3, EXTREAL2, SUPINF_1, FUNCT_7, REALSET1, RVSUM_1,
      MESFUNC1, SEQ_2;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
      VALUED_0, NAT_1, SUBSET_1, XCMPLX_0, PARTFUN1, XXREAL_0, RLVECT_1,
      STRUCT_0, NORMSP_1, MEASURE1, MESFUNC7;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
 definitions TARSKI, SUPINF_2, REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1,
      IDEAL_1, NORMSP_1, MEASURE6, MESFUNC5, MESFUNC6, SUBSET_1;
 theorems FUNCT_1, FUNCT_2, PARTFUN1, COMPLEX1, XBOOLE_0, TARSKI, RELAT_1,
      VALUED_1, IDEAL_1, RLSUB_1, ZFMISC_1, RLVECT_1, FUNCOP_1, XBOOLE_1,
      BINOP_1, SUPINF_2, RFUNCT_3, MESFUNC5, MESFUNC2, EXTREAL1, MEASURE1,
      MESFUNC6, PROB_1, RFUNCT_1, XXREAL_0, NUMBERS, ABSVALUE, MESFUNC1,
      MEASURE2, MESFUNC7, EXTREAL2, RSSPACE3, NORMSP_1, FUNCT_7;
 schemes BINOP_1, FUNCT_2;

begin :: Preliminaries of Real Linear Space

definition
  let V be non empty RLSStruct, V1 be Subset of V;
  attr V1 is multi-closed means :RLSUBDef0:
  for a be Real, v be VECTOR of V st v in V1 holds a*v in V1;
end;

theorem
  for V be RealLinearSpace, V1 be Subset of V holds
      V1 is linearly-closed iff V1 is add-closed multi-closed
proof
   let V be RealLinearSpace, V1 be Subset of V;
   hereby assume V1 is linearly-closed; then
    (for v,u be VECTOR of V st v in V1 & u in V1 holds v + u in V1) &
    (for a be Real,v be VECTOR of V st v in V1 holds a * v in V1)
      by RLSUB_1:def 1;
    hence V1 is add-closed & V1 is multi-closed by RLSUBDef0,IDEAL_1:def 1;
   end;
   assume V1 is add-closed & V1 is multi-closed; then
   (for v,u being Element of V st v in V1 & u in V1 holds v+u in V1) &
   (for a be Real, v be VECTOR of V st v in V1 holds a*v in V1)
     by RLSUBDef0,IDEAL_1:def 1;
   hence thesis by RLSUB_1:def 1;
end;

registration let V be non empty RLSStruct;
  cluster add-closed multi-closed non empty Subset of V;
  existence
  proof
    set M = the carrier of V;
    for u being set holds u in M implies u in the carrier of V;
    then reconsider M as Subset of V by TARSKI:def 3;
    reconsider M as non empty Subset of V;
    take M;
P1: for a be Real, v be VECTOR of V st v in M holds a*v in M;
    for x, y being Element of V st x in M & y in M holds x+y in M;
    hence thesis by P1,RLSUBDef0,IDEAL_1:def 1;
  end;
end;

definition
  let X be non empty RLSStruct;
  let X1 be multi-closed non empty Subset of X;
  func Mult_X1 -> Function of [:REAL,X1:], X1 equals
  (the Mult of X) | [:REAL,X1:];
correctness
proof
A2:[:REAL,X1:] c= [:REAL,the carrier of X:] by ZFMISC_1:118;
A3:dom the Mult of X = [:REAL,the carrier of X:] by FUNCT_2:def 1; then
A4:dom((the Mult of X)|[:REAL,X1:])=[:REAL,X1:] by A2,RELAT_1:91;
   now let z be set;
    assume A5: z in [:REAL,X1:]; then
    consider r,x be set such that
A6:  r in REAL & x in X1 & z=[r,x] by ZFMISC_1:def 2;
    reconsider y=x as VECTOR of X by A6;
    reconsider r as Real by A6;
    [r,x] in dom((the Mult of X)|[:REAL,X1:]) by A2,A3,A5,A6,RELAT_1:91;
    then ((the Mult of X)|[:REAL,X1:]).z = r*y by A6,FUNCT_1:70;
    hence ((the Mult of X)|[:REAL,X1:]).z in X1 by A6,RLSUBDef0;
   end;
   hence thesis by A4,FUNCT_2:5;
end;
end;

 reserve a,b,r for Real;

theorem RLSUB132:
for V be Abelian add-associative right_zeroed RealLinearSpace-like
    (non empty RLSStruct), V1 be non empty Subset of V,
    d1 be Element of V1, A be BinOp of V1, M be Function of [:REAL,V1:],V1 st
  d1 = 0.V & A = (the addF of V)|| V1 & M = (the Mult of V)|[:REAL,V1:]
holds RLSStruct(# V1,d1,A,M #) is
  Abelian add-associative right_zeroed RealLinearSpace-like
proof
   let V be Abelian add-associative right_zeroed RealLinearSpace-like
   (non empty RLSStruct),
   V1 be non empty Subset of V,
   d1 be Element of V1,
   A be BinOp of V1, M be Function of [:REAL,V1:],V1;
   set D = V1;
   assume that
A2: d1 = 0.V and
A3: A = (the addF of V)||V1 and
A4: M = (the Mult of V)|[:REAL,V1:];
   set W = RLSStruct(# D,d1,A,M #);
A6:now let x,y be VECTOR of W;
    thus x + y = (the addF of V).[x,y] by A3,FUNCT_1:72
              .= (the addF of V).(x,y);
   end;
A7:now let a; let x be VECTOR of W;
    thus a * x = (the Mult of V).[a,x] by A4,FUNCT_1:72
              .= (the Mult of V).(a,x);
   end;
   W is Abelian add-associative right_zeroed RealLinearSpace-like
   proof
    set Av = the addF of V; set Mv = the Mult of V;
    hereby let x,y be VECTOR of W;
     reconsider x1 = x, y1 = y as VECTOR of V by TARSKI:def 3;
     thus x + y = x1 + y1 by A6 .= y1 + x1 .= y + x by A6;
    end;
    now let x,y,z be VECTOR of W;
     reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by TARSKI:def 3;
     thus (x + y) + z = Av.(x + y,z1) by A6
                     .= (x1 + y1) + z1 by A6
                     .= x1 + (y1 + z1) by RLVECT_1:def 6
                     .= Av.(x1,y + z) by A6
                     .= x + (y + z) by A6;
    end;
    hence W is add-associative by RLVECT_1:def 6;
    now let x be VECTOR of W;
     reconsider y = x as VECTOR of V by TARSKI:def 3;
     thus x + 0.W = y + 0.V by A2,A6 .= x by RLVECT_1:def 7;
    end;
    hence W is right_zeroed by RLVECT_1:def 7;
    hereby let a; let x,y be VECTOR of W;
     reconsider x1 = x, y1 = y as VECTOR of V by TARSKI:def 3;
     thus a * (x + y) = Mv.(a,x + y) by A7 .= a * (x1 + y1) by A6
        .= a * x1 + a * y1 by RLVECT_1:def 9 .= Av.(Mv.(a,x1),a * y) by A7
        .= Av.(a * x, a * y) by A7.= a * x + a * y by A6;
    end;
    hereby let a,b; let x be VECTOR of W;
     reconsider y = x as VECTOR of V by TARSKI:def 3;
     thus (a + b) * x = (a + b) * y by A7
        .= a * y + b * y by RLVECT_1:def 9 .= Av.(Mv.(a,y),b * x) by A7
        .= Av.(a * x,b * x) by A7 .= a * x + b * x by A6;
    end;
    hereby let a,b; let x be VECTOR of W;
     reconsider y = x as VECTOR of V by TARSKI:def 3;
     thus (a * b) * x = (a * b) * y by A7 .= a * (b * y) by RLVECT_1:def 9
        .= Mv.(a,b * x) by A7 .= a * (b * x) by A7;
    end;
    let x be VECTOR of W;
    reconsider y = x as VECTOR of V by TARSKI:def 3;
    thus 1 * x = 1 * y by A7 .= x by RLVECT_1:def 9;
   end;
   hence thesis;
end;

theorem RSSPACE13:
for V be Abelian add-associative right_zeroed RealLinearSpace-like
 (non empty RLSStruct), V1 be add-closed multi-closed non empty Subset of V
 st 0.V in V1 holds
  RLSStruct (# V1,In (0.V, V1), add|(V1,V), Mult_ V1 #)
  is Abelian add-associative right_zeroed RealLinearSpace-like
proof
   let V be Abelian add-associative right_zeroed RealLinearSpace-like
   (non empty RLSStruct),
   V1 be add-closed multi-closed non empty Subset of V;
   assume 0.V in V1; then
   In(0.V,V1) = 0.V & Mult_V1 = (the Mult of V)|[:REAL,V1:] by FUNCT_7:def 1;
   hence thesis by RLSUB132;
end;

theorem RLSUB121:
for V be non empty RLSStruct,
    V1 be add-closed multi-closed non empty Subset of V,
    v,u be VECTOR of V,
  w1,w2 be VECTOR of RLSStruct (# V1,In(0.V,V1), add|(V1,V), Mult_ V1 #)
  st w1 = v & w2 = u holds w1 + w2 = v + u
proof
   let V be non empty RLSStruct, V1 be add-closed multi-closed
   non empty Subset of V, v,u be VECTOR of V,
    w1,w2 be VECTOR of RLSStruct (# V1,In (0.V, V1), add|(V1,V), Mult_ V1 #);
   assume A1: w1 = v & w2 = u; then
   [v,u] in [:V1,V1:] by ZFMISC_1:106;
   hence w1 + w2 = v+u by A1,FUNCT_1:72;
end;

theorem RLSUB122:
for V be non empty RLSStruct,
    V1 be add-closed multi-closed non empty Subset of V,
    a be Real, v be VECTOR of V,
    w be VECTOR of RLSStruct (# V1,In (0.V, V1), add|(V1,V), Mult_ V1 #) st
w = v holds a*w = a*v
proof
   let V be non empty RLSStruct, V1 be add-closed multi-closed
   non empty Subset of V, a be Real, v be VECTOR of V,
    w be VECTOR of RLSStruct (# V1,In (0.V, V1), add|(V1,V),Mult_ V1 #);
   assume A1: w = v; then
   [a,v] in [:REAL,V1:] & Mult_ V1 = (the Mult of V)|[:REAL,V1:]
     by ZFMISC_1:106;
   hence a*w = a*v by A1,FUNCT_1:72;
end;

begin :: Quasi-Real Linear Space of Partial Functions

reserve A,B for non empty set;
reserve f,g,h for Element of PFuncs(A,REAL);

definition
  let A,B; let F be BinOp of PFuncs(A,B), f,g be Element of PFuncs(A,B);
  redefine func F.(f,g) -> Element of PFuncs(A,B);
coherence
proof
   reconsider f,g as Element of PFuncs(A,B);
   F.(f,g) is Element of PFuncs(A,B);
   hence thesis;
end;
end;

definition let A;
  func multpfunc A -> BinOp of PFuncs(A,REAL) means :Def3:
  for f,g being Element of PFuncs(A,REAL) holds it.(f,g) = f(#)g;
existence
proof
   deffunc F(Element of PFuncs(A,REAL),Element of PFuncs(A,REAL)) = $1(#)$2;
   ex F being BinOp of PFuncs(A,REAL) st
    for f,g holds F.(f,g) = F(f,g) from BINOP_1:sch 4;
   hence thesis;
end;
uniqueness
proof
   let it1,it2 be BinOp of PFuncs(A,REAL) such that
A2: for f,g holds it1.(f,g) = f(#)g and
A3: for f,g holds it2.(f,g) = f(#)g;
   now let f,g;
    thus it1.(f,g) = f(#)g by A2 .=it2.(f,g) by A3;
   end;
   hence thesis by BINOP_1:2;
end;
end;

definition let A;
  func multrealpfunc A -> Function of [:REAL,PFuncs(A,REAL):],PFuncs(A,REAL)
  means :Def4:
  for a being Real, f being Element of PFuncs(A,REAL) holds it.(a,f) = a(#)f;
existence
proof
   deffunc F(Element of REAL,Element of PFuncs(A,REAL)) = $1(#)$2;
   ex F being Function of [:REAL,PFuncs(A,REAL):],PFuncs(A,REAL) st
    for a,f holds F.(a,f) = F(a,f) from BINOP_1:sch 4;
   hence thesis;
end;
uniqueness
proof
   let it1,it2 be Function of [:REAL,PFuncs(A,REAL):],PFuncs(A,REAL) such that
A2: for a being Real, f being Element of PFuncs(A,REAL) holds
     it1.(a,f) = a(#)f and
A3: for a being Real, f being Element of PFuncs(A,REAL) holds
     it2.(a,f) = a(#)f;
   now let a be Element of REAL, f be Element of PFuncs(A,REAL);
   thus it1.(a,f) = a(#)f by A2
                 .= it2.(a,f) by A3;
   end;
   hence thesis by BINOP_1:2;
end;
end;

definition let A;
  func RealPFuncZero A -> Element of PFuncs(A,REAL) equals A --> 0;
  coherence
proof
   A -->0 is Function of A,REAL by FUNCOP_1:58;
   hence thesis by PARTFUN1:119;
end;
end;

definition let A;
  func RealPFuncUnit A -> Element of PFuncs(A,REAL) equals A --> 1;
  coherence
proof
   A -->1 is Function of A,REAL by FUNCOP_1:58;
   hence thesis by PARTFUN1:119;
end;
end;

theorem Th10:
h = (addpfunc A).(f,g) iff (dom h= dom f /\ dom g &
   for x being Element of A st x in dom h holds h.x = f.x + g.x)
proof
   hereby assume A1: h = (addpfunc A).(f,g); then
    dom h = dom(f+g) by RFUNCT_3:def 4;
    hence dom h = dom f /\ dom g by VALUED_1:def 1;
    let x be Element of A;
    assume x in dom h; then
    x in dom (f+g) & h.x = (f+g).x by A1,RFUNCT_3:def 4;
    hence h.x = f.x + g.x by VALUED_1:def 1;
   end;
   assume
A6: dom h = dom f /\ dom g &
    for x being Element of A st x in dom h holds h.x=f.x + g.x;
   set k=(addpfunc A).(f,g);
A7:now let x be Element of A;
    assume A8: x in dom h; then
A10:x in dom(f+g) by A6,VALUED_1:def 1;
    k.x = (f+g).x by RFUNCT_3:def 4;
    hence k.x = f.x + g.x by A10,VALUED_1:def 1 .= h.x by A6,A8;
   end;
   dom k = dom (f+g) by RFUNCT_3:def 4 .= dom h by A6,VALUED_1:def 1;
   hence h = (addpfunc A).(f,g) by A7,PARTFUN1:34;
end;

theorem Th11:
h = (multpfunc A).(f,g) iff dom h = dom f /\ dom g &
  for x being Element of A st x in dom h holds h.x = f.x * g.x
proof
   hereby assume A2: h = (multpfunc A).(f,g);
    hence
     dom h = dom (f(#)g) by Def3 .= dom f /\ dom g by VALUED_1:def 4;
    let x be Element of A;
    assume x in dom h; then
A5: x in dom (f(#)g) by A2,Def3;
    h.x = (f(#)g).x by A2,Def3;
    hence h.x = f.x * g.x by A5,VALUED_1:def 4;
   end;
   assume
A7: dom h = dom f /\ dom g & for x being Element of A st x in dom h holds
    h.x=f.x * g.x;
   set k=(multpfunc A).(f,g);
A8:now let x be Element of A;
    assume A9: x in dom h; then
A10:x in dom (f(#)g) by A7,VALUED_1:def 4;
    k.x = (f(#)g).x by Def3;
    hence k.x = f.x * g.x by A10,VALUED_1:def 4 .= h.x by A7,A9;
   end;
   dom k = dom(f(#)g) by Def3 .= dom h by A7,VALUED_1:def 4;
   hence h = (multpfunc A).(f,g) by A8,PARTFUN1:34;
end;

theorem
RealPFuncZero A <> RealPFuncUnit A
proof
   consider a being Element of A;
   (RealPFuncZero A).a=0 & (RealPFuncUnit A).a=1 by FUNCOP_1:13;
   hence thesis;
end;

theorem Th15:
h = (multrealpfunc A).(a,f) iff dom h = dom f &
  for x being Element of A st x in dom f holds h.x = a * f.x
proof
   hereby assume A0: h = (multrealpfunc A).(a,f); then
    dom h = dom(a(#)f) by Def4;
    hence dom h = dom f by VALUED_1:def 5;
    let x be Element of A;
    assume x in dom f; then
    x in dom(a(#)f) by VALUED_1:def 5; then
    (a(#)f).x = a*(f.x) by VALUED_1:def 5;
    hence h.x = a*(f.x) by A0,Def4;
   end;
   hereby assume
A1:  dom f = dom h & for x being Element of A st x in dom f holds h.x = a*f.x;
    reconsider k= (multrealpfunc A).(a,f) as Element of PFuncs(A,REAL);
A2: now let x be Element of A;
     assume A3:x in dom f; then
     x in dom(a(#)f) by VALUED_1:def 5; then
     (a(#)f).x = a * f.x by VALUED_1:def 5; then
     (a(#)f).x = h.x by A1,A3;
     hence k.x = h.x by Def4;
    end;
    k = a(#)f by Def4; then
    dom k = dom f by VALUED_1:def 5;
    hence h = (multrealpfunc A).(a,f) by A1,A2,PARTFUN1:34;
   end;
end;

theorem Th16:
(addpfunc A).(f,g) = (addpfunc A).(g,f)
proof
   addpfunc A is commutative by RFUNCT_3:16;
   hence thesis by BINOP_1:def 2;
end;

theorem Th17:
(addpfunc A).(f,(addpfunc A).(g,h)) = (addpfunc A).((addpfunc A).(f,g),h)
proof
   addpfunc A is associative by RFUNCT_3:17;
   hence thesis by BINOP_1:def 3;
end;

theorem
(multpfunc A).(f,g) = (multpfunc A).(g,f)
proof
A1:dom((multpfunc A).(f,g)) = dom f/\ dom g by Th11;
A2:dom((multpfunc A).(g,f)) = dom g/\ dom f by Th11;
   now let x be Element of A;
    assume A3: x in dom f /\ dom g;
    hence ((multpfunc A).(f,g)).x = g.x * f.x by A1,Th11
                                 .= ((multpfunc A).(g,f)).x by A2,A3,Th11;
   end;
   hence thesis by A1,A2,PARTFUN1:34;
end;

theorem
(multpfunc A).(f,(multpfunc A).(g,h)) = (multpfunc A).((multpfunc A).(f,g),h)
proof
   set j = (multpfunc A).(g,h); set k = (multpfunc A).(f,g);
   set j1 = (multpfunc A).(f,j); set k1 = (multpfunc A).(k,h);
A2:dom j1 = dom f /\ dom j & dom k1 = dom k /\ dom h by Th11; then
A3:dom j1 = dom f/\(dom g /\dom h) & dom k1 = (dom f /\ dom g)/\dom h by Th11;
A6:dom j1 c= dom j & dom k1 c= dom k by A2,XBOOLE_1:17;
   now let x be Element of A;
    assume A8: x in dom j1;
A11:x in dom k1 by A3,A8,XBOOLE_1:16;
    thus j1.x =f.x * j.x by Th11,A8
     .= f.x * (g.x * h.x) by Th11,A6,A8
     .= (f.x * g.x) * h.x
     .= k.x * h.x by Th11,A6,A11
     .= k1.x by Th11,A11;
   end;
   hence thesis by A3,PARTFUN1:34,XBOOLE_1:16;
end;

theorem
(multpfunc A).(RealPFuncUnit A,f) = f
proof
   set h = (multpfunc A).(RealPFuncUnit A,f);
   dom h = dom(RealPFuncUnit A) /\ dom f by Th11; then
   dom h = A /\ dom f by FUNCOP_1:19; then
A4:dom h = dom f by XBOOLE_1:28;
   now let x be Element of A;
    assume x in dom f; then
    h.x = (RealPFuncUnit A).x * f.x by A4,Th11; then
    h.x = 1 * f.x by FUNCOP_1:13;
    hence h.x = f.x;
   end;
   hence thesis by A4,PARTFUN1:34;
end;

theorem Th21:
(addpfunc A).(RealPFuncZero A,f) = f
proof
   set h = (addpfunc A).(RealPFuncZero A,f);
   dom h = dom(RealPFuncZero A) /\ dom f by Th10; then
   dom h = A /\ dom f by FUNCOP_1:19; then
A4:dom h = dom f by XBOOLE_1:28;
   now let x be Element of A;
    assume A5: x in dom f;
    (RealPFuncZero A).x = 0 by FUNCOP_1:13;
    hence h.x=0+ f.x by A4,A5,Th10 .= f.x;
   end;
   hence thesis by A4,PARTFUN1:34;
end;

theorem Th22:
(addpfunc A).(f,(multrealpfunc A).(-1,f)) = (RealPFuncZero A)|(dom f)
proof
   reconsider g = (multrealpfunc A).(-1,f) as Element of PFuncs(A,REAL);
   set h = (addpfunc A).(f,g);
   dom (RealPFuncZero A) = A by FUNCOP_1:19; then
   dom ((RealPFuncZero A)|(dom f)) = A /\ dom f by FUNCT_1:68; then
A4:dom ((RealPFuncZero A)|(dom f)) = dom f by XBOOLE_1:28;
A5:dom h = dom g /\ dom f by Th10 .= dom f /\ dom f by Th15;
   now let x be Element of A;
    assume A7: x in dom f; then
A12:x in dom((-1)(#)f) by VALUED_1:def 5;
    thus h.x = f.x + g.x by Th10,A7,A5
       .= f.x + ((-1)(#)f).x by Def4
       .= f.x + (-1) * f.x by A12,VALUED_1:def 5
       .= (RealPFuncZero A).x by FUNCOP_1:13
       .= ((RealPFuncZero A)|(dom f)).x by A7,FUNCT_1:72;
   end;
   hence thesis by A4,A5,PARTFUN1:34;
end;

theorem Th23:
(multrealpfunc A).(1,f) = f
proof
   reconsider g = (multrealpfunc A).(1 qua Real,f)
     as Element of PFuncs(A,REAL);
A1:dom g=dom f by Th15;
   now let x be Element of A;
    assume x in dom f;
    hence g.x = 1*(f.x) by Th15 .= f.x;
   end;
   hence thesis by A1,PARTFUN1:34;
end;

theorem Th24:
(multrealpfunc A).(a,(multrealpfunc A).(b,f)) = (multrealpfunc A).(a*b,f)
proof
   reconsider g = (multrealpfunc A).(b,f) as Element of PFuncs(A,REAL);
   reconsider h = (multrealpfunc A).(a,g) as Element of PFuncs(A,REAL);
   reconsider k = (multrealpfunc A).(a*b,f) as Element of PFuncs(A,REAL);
A1:dom g = dom f & dom h = dom g & dom k = dom f by Th15;
   now let x be Element of A;
    assume A4: x in dom h;
    hence h.x =a*(g.x) by A1,Th15 .=a*(b*(f.x)) by A4,A1,Th15
            .=(a*b)*(f.x) .= k.x by A1,A4,Th15;
   end;
   hence thesis by A1,PARTFUN1:34;
end;

theorem Th25:
(addpfunc A).((multrealpfunc A).(a,f),(multrealpfunc A).(b,f))
  = (multrealpfunc A).(a+b,f)
proof
   reconsider g = (multrealpfunc A).(a,f) as Element of PFuncs(A,REAL);
   reconsider h = (multrealpfunc A).(b,f) as Element of PFuncs(A,REAL);
   reconsider k = (multrealpfunc A).(a+b,f) as Element of PFuncs(A,REAL);
   set j = (addpfunc A).(g,h);
A1:dom g = dom f & dom h = dom f & dom k = dom f by Th15; then
   dom h /\ dom g = dom f /\ dom f; then
A3:dom j = dom f by Th10;
   now let x be Element of A;
    assume A5: x in dom j; then
    x in dom(a(#)f) & x in dom(b(#)f) by A3,VALUED_1:def 5; then
    (a(#)f).x = a*f.x & (b(#)f).x = b*f.x by VALUED_1:def 5; then
    g.x = a*f.x & h.x = b*f.x by Def4; then
    g.x + h.x = (a+b)*(f.x);
    hence j.x = (a+b)*(f.x) by Th10,A5 .= k.x by Th15,A3,A5;
   end;
   hence thesis by A1,A3,PARTFUN1:34;
end;

Lm2:
(addpfunc A).((multrealpfunc A).(a,f),(multrealpfunc A).(a,g))
  = (multrealpfunc A).(a,(addpfunc A).(f,g))
proof
   reconsider h = (multrealpfunc A).(a,f) as Element of PFuncs(A,REAL);
   reconsider i = (multrealpfunc A).(a,g) as Element of PFuncs(A,REAL);
   set j = (addpfunc A).(f,g);
   reconsider k = (multrealpfunc A).(a,j) as Element of PFuncs(A,REAL);
   set l = (addpfunc A).(h,i);
A1:dom h = dom f & dom i = dom g & dom k = dom j by Th15;
A3:dom j = dom f /\ dom g & dom l = dom h /\ dom i by Th10;
   now let x be Element of A;
    assume A9: x in dom l; then
B2: x in dom(f+g) by A1,A3,VALUED_1:def 1;
    x in dom h & x in dom i by A9,A3,XBOOLE_0:def 4; then
    x in dom f & x in dom g by Th15; then
A11:x in dom (a(#)f) & x in dom (a(#)g) by VALUED_1:def 5;
    h.x = (a(#)f).x & i.x = (a(#)g).x by Def4; then
A12:h.x = a * f.x & i.x = a * g.x by A11,VALUED_1:def 5;
    thus l.x = h.x + i.x by A9,Th10
    .= a*(f.x+g.x) by A12
    .= a*(f+g).x by B2,VALUED_1:def 1
    .= a*j.x by RFUNCT_3:def 4
    .= k.x by A9,A1,A3,Th15;
   end;
   hence thesis by A1,A3,PARTFUN1:34;
end;

theorem
(multpfunc A).(f,(addpfunc A).(g,h))
 = (addpfunc A).((multpfunc A).(f,g),(multpfunc A).(f,h))
proof
   set i = (multpfunc A).(f,h); set j = (multpfunc A).(f,g);
   set k = (addpfunc A).(j,i);  set l = (addpfunc A).(g,h);
   set m = (multpfunc A).(f,l);
A1:dom i = dom f /\ dom h & dom j = dom f /\ dom g &
   dom m = dom f /\ dom l by Th11;
A2:dom k = dom j /\ dom i & dom l = dom g /\ dom h by Th10;
   dom k = (dom h /\ dom f) /\ (dom f /\ dom g) by A1,Th10; then
   dom k = dom h /\ (dom f /\ (dom f /\ dom g)) by XBOOLE_1:16; then
A3:dom k = dom h /\ (dom f /\ dom f /\ dom g) by XBOOLE_1:16;
A6:dom f /\ dom g /\ dom h = dom f /\ (dom g /\ dom h) &
   dom f /\ dom g /\ dom h = dom g /\ (dom f /\ dom h) by XBOOLE_1:16;
   now let x be Element of A;
    assume
A14: x in dom k; then
    x in dom f /\ dom g & x in dom f /\ dom h & x in dom g /\ dom h &
    x in dom f /\ dom l by A3,A6,Th10,XBOOLE_0:def 4; then
B1: x in dom(f(#)g) & x in dom(f(#)h) & x in dom(g+h) & x in dom(f(#)l)
      by VALUED_1:def 1,def 4;
    j.x = (f(#)g).x & i.x = (f(#)h).x by Def3; then
A22:j.x = f.x * g.x & i.x = f.x * h.x by B1,VALUED_1:def 4;
A24:l.x = (g+h).x by RFUNCT_3:def 4;
A25:m.x = (f(#)l).x by Def3;
    k.x = j.x + i.x by Th10,A14; then
    k.x = f.x * (g.x + h.x) by A22; then
    k.x = f.x * l.x by A24,B1,VALUED_1:def 1;
    hence k.x = m.x by A25,B1,VALUED_1:def 4;
   end;
   hence thesis by A3,A1,A2,PARTFUN1:34,XBOOLE_1:16;
end;

theorem
(multpfunc A).((multrealpfunc A).(a,f),g)
 = (multrealpfunc A).(a,(multpfunc A).(f,g))
proof
   reconsider i = (multrealpfunc A).(a,f) as Element of PFuncs(A,REAL);
   set j = (multpfunc A).(f,g); set k = (multpfunc A).(i,g);
   reconsider l = (multrealpfunc A).(a,j) as Element of PFuncs(A,REAL);
A1:dom i = dom f & dom l = dom j by Th15;
A3:dom k = dom i /\ dom g & dom j = dom f /\ dom g by Th11;
   now let x be Element of A;
    assume
A5:  x in dom k; then
A6: x in dom f & x in dom g & x in dom(f(#)g) & x in dom(a(#)j)
      by A1,A3,VALUED_1:def 4,def 5,XBOOLE_0:def 4;
    j.x = (f(#)g).x by Def3; then
A10:j.x = f.x * g.x by A6,VALUED_1:def 4;
    i.x = (a(#)f).x & dom (a(#)f) = dom f by Def4,VALUED_1:def 5; then
A9: i.x = a * f.x by A6,VALUED_1:def 5;
    l.x = (a(#)j).x by Def4; then
A12:l.x = a*(f.x * g.x) by A6,A10,VALUED_1:def 5;
    k.x =i.x * g.x by Th11,A5;
    hence k.x = l.x by A9,A12;
   end;
   hence thesis by A1,A3,PARTFUN1:34;
end;

definition let A;
  func RLSp_PFunctA -> non empty RLSStruct equals
    RLSStruct(#PFuncs(A,REAL), RealPFuncZero A, addpfunc A, multrealpfunc A#);
  coherence;
end;

reserve u,v,w for VECTOR of RLSp_PFunctA;

registration let A;
  cluster RLSp_PFunctA -> strict Abelian add-associative right_zeroed
               RealLinearSpace-like;
  coherence
  proof
   set IT = RLSp_PFunctA;
   thus IT is strict;
   thus u+v = v+u by Th16;
   thus u+v+w = u+(v+w) by Th17;
   thus u+0.IT = u
   proof
    reconsider u'=u as Element of PFuncs(A,REAL);
    thus u+0.IT = (addpfunc(A)).(RealPFuncZero(A),u') by Th16
               .= u by Th21;
   end;
   thus a*(u+v) = a*u + a *v by Lm2;
   thus (a+b)*v = a*v + b*v by Th25;
   thus (a*b)*v = a*(b*v) by Th24;
   thus 1*v = v by Th23;
end;
end;

begin :: Quasi-Real Linear Space of Integrable Functions

reserve X for non empty set,
        x for Element of X,
        S for SigmaField of X,
        M for sigma_Measure of S,
        E,E1,E2,A,B for Element of S,
        f,g,h,f1,g1 for PartFunc of X,REAL;

theorem Lm1:
for X,S,M for f be PartFunc of X,ExtREAL st
 (ex E st E = dom f) & for x st x in dom f holds 0= f.x holds
  f is_integrable_on M & Integral(M,f) = 0
proof
   let X,S,M;
   let f be PartFunc of X,ExtREAL;
   assume A1: ex E st E = dom f;
   assume A2: for x st x in dom f holds 0 = f.x;
   consider E be Element of S such that
A3: E = dom f by A1;
A5:for x be set st x in dom f holds f.x = 0 by A2; then
A4:f is_simple_func_in S by A1,MESFUNC6:2;
A6:f is_measurable_on E by A1,A5,MESFUNC2:37,MESFUNC6:2;
A7:dom max+f = dom f & for x be Element of X st x in dom max+f holds
    (max+f).x = max(f.x,0.) by MESFUNC2:def 2;
A8:now let x be Element of X;
    assume A9: x in dom f;
    hence f.x = max(0,0) by A2 .=max(f.x,0) by A2,A9 .= (max+f).x by A7,A9;
   end;
A10:integral+(M,f) = 0 by A1,A2,A4,MESFUNC2:37,MESFUNC5:93;
A11:f is nonnegative
   proof
    let y be R_eal;
    assume y in rng f; then
    ex x1 being set st x1 in dom f & y = f.x1 by FUNCT_1:def 5;
    hence y >= 0 by A2;
   end; then
A13: 0. = Integral(M,f) by A1,A4,A10,MESFUNC2:37,MESFUNC5:94
       .= integral+(M,f)-integral+(M,max-f) by A7,A8,PARTFUN1:34
       .= 0.+(-integral+(M,max-f)) by A1,A2,A4,MESFUNC2:37,MESFUNC5:93
       .= -integral+(M,max-f) by SUPINF_2:18;
   integral+(M,max+f) < +infty by A7,A8,A10,PARTFUN1:34;
   hence thesis by A3,A6,A10,A11,A13,EXTREAL1:24,MESFUNC5:94,def 17;
end;

definition
  let X be non empty set, r be Real;
redefine func X --> r -> PartFunc of X,REAL;
coherence
proof
   thus X --> r is PartFunc of X,REAL;
end;
end;

Lm2:
 (X = dom f & for x st x in dom f holds 0 = f.x) implies
  f is_integrable_on M & Integral(M,f) =0
proof
   assume A1:X=dom f & for x st x in dom f holds 0 = f.x;
   X is Element of S by MEASURE1:21; then
   R_EAL f is_integrable_on M & Integral(M,R_EAL f) = 0 by Lm1,A1;
   hence thesis by MESFUNC6:def 9;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
 func L1_Functions M -> non empty Subset of RLSp_PFunctX equals
  { f where f is PartFunc of X,REAL : ex ND be Element of S st M.ND=0 &
  dom f = ND` & f is_integrable_on M };
correctness
proof
   set I = { f where f is PartFunc of X,REAL : ex ND be Element of S st
       M.ND=0 & dom f = ND` & f is_integrable_on M };
A1:I c= PFuncs(X,REAL)
   proof
    let x be set;
    assume x in I; then
    ex f be PartFunc of X,REAL st x = f &
     ex ND be Element of S st M.ND=0 & dom f = ND` & f is_integrable_on M;
    hence x in PFuncs(X,REAL) by PARTFUN1:119;
   end;
   set g = X --> 0;
   reconsider ND = {} as Element of S by MEASURE1:66;
A3:M.ND =0 by MEASURE1:def 11;
A4:dom g = ND` by FUNCOP_1:19;
   for x be Element of X st x in dom g holds g.x = 0 by FUNCOP_1:13; then
   g is_integrable_on M by A4,Lm2; then
   g in I by A3,A4;
   hence thesis by A1;
end;
end;

LmDef1:
X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M
proof
   reconsider g = X --> 0 as Function of X,REAL by FUNCOP_1:58;
   reconsider ND = {} as Element of S by MEASURE1:66;
A1:M.ND =0 by MEASURE1:def 11;
A2:dom g = ND` by FUNCT_2:def 1;
   for x be Element of X st x in dom g holds g.x = 0 by FUNCOP_1:13; then
   g is_integrable_on M by A2,Lm2;
   hence thesis by A1,A2;
end;

MLm01:
M.E1=0 & M.E2=0 implies M.(E1\/E2) =0
proof
   assume M.E1=0 & M.E2=0; then
   E1 is measure_zero of M & E2 is measure_zero of M by MEASURE1:def 13; then
   E1 \/ E2 is measure_zero of M by MEASURE1:70;
   hence M.(E1 \/ E2) = 0 by MEASURE1:def 13;
end;

theorem Th01a:
f in L1_Functions M & g in L1_Functions M implies
  f + g in L1_Functions M
proof
   set W = L1_Functions M;
   assume A1: f in W & g in W; then
   ex f1 be PartFunc of X,REAL st
    f1=f &ex ND be Element of S st M.ND=0 & dom f1 = ND` &
    f1 is_integrable_on M; then
   consider NDv be Element of S such that
A3: M.NDv=0 & dom f = NDv` & f is_integrable_on M;
   ex g1 be PartFunc of X,REAL st
    g1=g &ex ND be Element of S st M.ND=0 & dom g1 = ND` &
    g1 is_integrable_on M by A1; then
   consider NDu be Element of S such that
A5: M.NDu=0 & dom g = NDu` & g is_integrable_on M;
A6:M.(NDv \/ NDu) =0 & f+g is_integrable_on M by A3,A5,MLm01,MESFUNC6:100;
   dom (f+g)= NDv` /\ NDu` by A5,A3,VALUED_1:def 1
              .= (NDv \/ NDu)` by XBOOLE_1:53;
   hence thesis by A6;
end;

theorem Th01b:
f in L1_Functions M implies a(#)f in L1_Functions M
proof
   set W = L1_Functions M;
   assume f in W; then
   ex f1 be PartFunc of X,REAL st
    f1=f & ex ND be Element of S st M.ND=0 & dom f1 = ND` &
    f1 is_integrable_on M; then
   consider ND be Element of S such that
A3: M.ND=0 & dom f = ND` & f is_integrable_on M;
   dom (a(#)f) = ND` & a(#)f is_integrable_on M
     by A3,MESFUNC6:102,VALUED_1:def 5;
   hence thesis by A3;
end;

Th01: L1_Functions M is add-closed & L1_Functions M is multi-closed
proof
   set W = L1_Functions M;
   now let v,u be Element of the carrier of RLSp_PFunctX such that
A2: v in W & u in W;
    consider v1 be PartFunc of X, REAL such that
A3:  v1=v & ex ND be Element of S st M.ND=0 & dom v1 = ND` &
     v1 is_integrable_on M by A2;
    consider u1 be PartFunc of X, REAL such that
A4:  u1=u & ex ND be Element of S st M.ND=0 & dom u1 = ND` &
     u1 is_integrable_on M by A2;
    reconsider h = v+u as Element of PFuncs(X,REAL);
    dom h = dom v1 /\ dom u1 &
    for x be set st x in dom h holds h.x = v1.x + u1.x by A3,A4,Th10; then
    v+u=v1+u1 by VALUED_1:def 1;
    hence v+u in L1_Functions M by A2,A3,A4,Th01a;
   end;
   hence L1_Functions M is add-closed by IDEAL_1:def 1;
   now let a be Real, u be VECTOR of RLSp_PFunctX such that
A7:  u in W;
    consider u1 be PartFunc of X, REAL such that
A8:  u1=u & ex ND be Element of S st M.ND=0 & dom u1 = ND` &
     u1 is_integrable_on M by A7;
    reconsider h = a*u as Element of PFuncs(X,REAL);
A9: dom h = dom u1 &
    for x being Element of X st x in dom u1 holds h.x = a * (u1.x)
      by A8,Th15; then
    for x be set st x in dom h holds h.x = a*(u1.x); then
    a*u=a(#)u1 by A9,VALUED_1:def 5;
    hence a*u in L1_Functions M by Th01b,A7,A8;
   end;
   hence L1_Functions M is multi-closed by RLSUBDef0;
end;

registration
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  cluster L1_Functions M -> multi-closed add-closed;
  coherence by Th01;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  func RLSp_L1Funct M -> non empty RLSStruct equals
  RLSStruct (# L1_Functions M,
               In (0.(RLSp_PFunctX), L1_Functions M),
               add|(L1_Functions M,RLSp_PFunctX),
               Mult_(L1_Functions M) #);
  coherence;
end;

registration
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  cluster RLSp_L1Funct M ->
    strict Abelian add-associative right_zeroed RealLinearSpace-like;
coherence
proof
   0.(RLSp_PFunctX) in L1_Functions M by LmDef1;
   hence thesis by RSSPACE13;
end;
end;

begin :: Quotient Space of Quasi-Real Linear Space of Integrable Functions

reserve v,u for VECTOR of RLSp_L1Funct M;

theorem ThB10:
f=v & g=u implies f+g=v+u
proof
assume A1:f=v & g=u;
   reconsider v2=v as VECTOR of RLSp_PFunct(X) by TARSKI:def 3;
   reconsider u2=u as VECTOR of RLSp_PFunct(X) by TARSKI:def 3;
   reconsider h = v2+u2 as Element of PFuncs(X,REAL);
   reconsider v3= v2 as Element of PFuncs(X,REAL);
   reconsider u3= u2 as Element of PFuncs(X,REAL);
A3:dom h= dom v3 /\ dom u3 &
   for x being Element of X st x in dom h holds h.x = v3.x + u3.x by Th10;
   for x be set st x in dom h holds h.x = f.x + g.x by A1,Th10; then
   h= f+g by A1,A3,VALUED_1:def 1;
   hence thesis by RLSUB121;
end;

theorem ThB11:
f=u implies a(#)f=a*u
proof
   reconsider u2=u as VECTOR of RLSp_PFunctX by TARSKI:def 3;
   reconsider h = a*u2 as Element of PFuncs(X,REAL);
   assume A1:f=u; then
A3:dom h = dom f by Th15; then
   for x be set st x in dom h holds h.x = a*(f.x) by A1,Th15; then
   h= a(#)f by A3,VALUED_1:def 5;
   hence thesis by RLSUB122;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
      f,g be PartFunc of X,REAL;
  pred f a.e.= g,M means :Def2:
    ex E be Element of S st M.E = 0 & f|E` = g|E`;
end;

theorem ThB11Z:
 f=u implies
  u+(-1)*u = (X --> 0)|dom f &
  ex v,g be PartFunc of X,REAL st
   v in L1_Functions M & g in L1_Functions M &
   v = u+(-1)*u & g = X --> 0 & v a.e.= g,M
proof
   reconsider u2=u as VECTOR of RLSp_PFunctX by TARSKI:def 3;
   reconsider h = u2+(-1)*u2 as Element of PFuncs(X,REAL);
   assume A1: f=u; then
A2:h = (RealPFuncZero X)|dom f & (-1)*u2=(-1)*u by Th22,RLSUB122;
   hence u+(-1)*u = (X --> 0)|dom f by RLSUB121;
   u+(-1)*u in L1_Functions M; then
   consider v be PartFunc of X,REAL such that
A4: v=u+(-1)*u &
    ex ND be Element of S st M.ND=0 & dom v = ND` & v is_integrable_on M;
   u in L1_Functions M; then
   ex uu1 be PartFunc of X,REAL st
    uu1=u & ex ND be Element of S st M.ND=0 & dom uu1 = ND` &
    uu1 is_integrable_on M; then
   consider ND be Element of S such that
A6: M.ND=0 & dom f = ND` & f is_integrable_on M by A1;
   set g = X-->0;
A7:g in L1_Functions M by LmDef1;
   v|ND` = g|ND`|ND` by RLSUB121,A2,A4,A6; then
   v|ND` = g|ND` by FUNCT_1:82; then
   v a.e.= g,M by Def2,A6;
   hence thesis by A4,A7;
end;

theorem Th04:
f a.e.= f,M
proof
   {} is Element of S by PROB_1:10; then
   consider E being Element of S such that
A1: E = {};
A2:M.E = 0 by A1,MEASURE1:def 11;
   f|E` = f|E`;
   hence thesis by A2,Def2;
end;

theorem Th05:
f a.e.= g,M implies g a.e.= f,M
proof
   assume f a.e.= g,M; then
   ex E be Element of S st M.E = 0 & f|E` = g|E` by Def2;
   hence g a.e.= f,M by Def2;
end;

theorem Th06:
f a.e.= g,M & g a.e.= h,M implies f a.e.= h,M
proof
   assume that
A1: f a.e.= g,M and
A2: g a.e.= h,M;
   consider EQ1 being Element of S such that
A3: M.EQ1=0 & f|EQ1` = g|EQ1` by Def2,A1;
   consider EQ2 being Element of S such that
A4: M.EQ2=0 & g|EQ2` = h|EQ2` by Def2,A2;
A7:M.(EQ1 \/ EQ2) = 0 by A3,A4,MLm01;
A8:(EQ1\/EQ2)` c= EQ1` & (EQ1\/EQ2)` c= EQ2` by XBOOLE_1:7,34; then
   f|(EQ1\/EQ2)` =g|EQ1`|(EQ1\/EQ2)` by A3,FUNCT_1:82
     .=g|(EQ1\/EQ2)` by A8,FUNCT_1:82
     .=h|EQ2`|(EQ1\/EQ2)` by A4,A8,FUNCT_1:82
     .=h|(EQ1\/EQ2)` by A8,FUNCT_1:82;
   hence thesis by A7,Def2;
end;

theorem Th07:
f a.e.= f1,M & g a.e.= g1,M implies (f+g) a.e.= (f1+g1),M
proof
   assume that
A1: f a.e.= f1,M and
A2: g a.e.= g1,M;
   consider EQ1 being Element of S such that
A3: M.(EQ1)=0 & f|EQ1` =f1|EQ1` by A1,Def2;
   consider EQ2 being Element of S such that
A4: M.(EQ2)=0 & g|EQ2` =g1|EQ2` by A2,Def2;
A7:M.(EQ1 \/ EQ2) = 0 by A3,A4,MLm01;
A8:(EQ1\/EQ2)` c= EQ1` & (EQ1\/EQ2)` c= EQ2` by XBOOLE_1:7,34; then
   f|(EQ1\/EQ2)` =f1|EQ1`|(EQ1\/EQ2)` by A3,FUNCT_1:82; then
A9:f|(EQ1\/EQ2)` =f1|(EQ1\/EQ2)` by A8,FUNCT_1:82;
   g|(EQ1\/EQ2)` =g1|EQ2`|(EQ1\/EQ2)` by A4,A8,FUNCT_1:82
      .=g1|(EQ1\/EQ2)` by A8,FUNCT_1:82; then
   (f+g)|(EQ1\/EQ2)` =f1|(EQ1\/EQ2)` + g1|(EQ1\/EQ2)`
     by A9,RFUNCT_1:60 .=(f1+g1)|(EQ1\/EQ2)` by RFUNCT_1:60;
   hence thesis by Def2,A7;
end;

theorem Th08:
f a.e.= g,M implies a(#)f a.e.= a(#)g,M
proof
   assume f a.e.= g,M; then
   consider E being Element of S such that
A2: M.E = 0 & f|E`=g|E` by Def2;
   (a(#)f)|E` = a(#)(g|E`) by A2,RFUNCT_1:65
     .= (a(#)g)|E` by RFUNCT_1:65;
   hence thesis by A2,Def2;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func AlmostZeroFunctions M ->
      non empty Subset of RLSp_L1Funct M equals
  { f where f is PartFunc of X,REAL : f in L1_Functions M &
      f a.e.= X-->0,M };
coherence
proof
A1:now let x be set;
    assume x in { f where f is PartFunc of X,REAL: f in L1_Functions M &
               f a.e.= X-->0,M }; then
    ex f be PartFunc of X,REAL st
     x=f & f in L1_Functions M & f a.e.= X-->0,M;
    hence x in the carrier of RLSp_L1Funct M;
   end;
A3:X-->0 a.e.= X-->0,M by Th04;
   X-->0 in L1_Functions M by LmDef1; then
   X-->0 in { f where f is PartFunc of X,REAL :
           f in L1_Functions M & f a.e.= X-->0,M } by A3;
   hence thesis by A1,TARSKI:def 3;
end;
end;

theorem HSATZE:
(X-->0) + (X-->0) = X-->0 & a(#)(X-->0) = X-->0
proof
   set g1 = X-->0; set g2 = X-->0;
B1:dom(g1+g2) = dom g1 /\ dom g2 by VALUED_1:def 1;
   now let x be Element of X;
    assume x in dom(X --> 0); then
    (g1+g2).x = g1.x + g2.x by B1,VALUED_1:def 1; then
    (g1+g2).x = 0 + g2.x by FUNCOP_1:13;
    hence (g1+g2).x = (X --> 0).x;
   end;
   hence g1+g2 = X-->0 by B1,PARTFUN1:34;
B2:dom(a(#)g1) = dom(X-->0) by VALUED_1:def 5;
   now let x be Element of X;
    assume x in dom(a(#)g1); then
    (a(#)g1).x = a * g1.x by VALUED_1:def 5; then
    (a(#)g1).x = a * 0 by FUNCOP_1:13;
    hence (a(#)g1).x = (X --> 0).x by FUNCOP_1:13;
   end;
   hence thesis by B2,PARTFUN1:34;
end;

Th09:
AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed
proof
   set Z = AlmostZeroFunctions M;
   set V = RLSp_L1Funct M;
   now let v,u be VECTOR of V such that
A2:  v in Z & u in Z;
    consider v1 be PartFunc of X, REAL such that
A3:  v1=v & v1 in L1_Functions M & v1 a.e.= X-->0,M by A2;
    consider u1 be PartFunc of X, REAL such that
A4:  u1=u & u1 in L1_Functions M & u1 a.e.= X-->0,M by A2;
A5: v+u=v1+u1 by ThB10,A3,A4;
    (X-->0)+(X-->0)=X-->0 by HSATZE; then
    v1+u1 in L1_Functions M & v1+u1 a.e.=X-->0,M by A5,A3,A4,Th07;
    hence v+u in Z by A5;
   end;
   hence Z is add-closed by IDEAL_1:def 1;
   now let a be Real, u be VECTOR of V;
    assume u in Z; then
    consider u1 be PartFunc of X, REAL such that
A10: u1=u & u1 in L1_Functions M & u1 a.e.= X-->0,M;
A11:a*u=a(#)u1 by ThB11,A10;
    a(#)(X-->0)=X-->0 by HSATZE; then
    a(#)u1 in L1_Functions M & a(#)u1 a.e.=X-->0,M by A11,A10,Th08;
    hence a*u in Z by A11;
   end;
   hence Z is multi-closed by RLSUBDef0;
end;

registration
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  cluster AlmostZeroFunctions M -> add-closed multi-closed;
  coherence by Th09;
end;

theorem Th09a:
0.(RLSp_L1Funct M) = X-->0 &
0.(RLSp_L1Funct M) in AlmostZeroFunctions M
proof
   thus 0.(RLSp_L1Funct M) = X --> 0 by LmDef1,FUNCT_7:def 1;
A2:X-->0 a.e.= X-->0,M & X --> 0 in L1_Functions M by Th04,LmDef1;
   0.(RLSp_L1Funct M) = 0.(RLSp_PFunctX) by LmDef1,FUNCT_7:def 1;
   hence 0.(RLSp_L1Funct M) in AlmostZeroFunctions M by A2;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  func RLSp_AlmostZeroFunct M -> non empty RLSStruct equals
   RLSStruct (# AlmostZeroFunctions M,
                In(0.(RLSp_L1Funct M),AlmostZeroFunctions M),
                add|(AlmostZeroFunctions M,RLSp_L1Funct M),
                Mult_(AlmostZeroFunctions M) #);
  coherence;
end;

registration
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  cluster RLSp_L1Funct M ->
    strict strict Abelian add-associative right_zeroed RealLinearSpace-like;
  coherence;
end;

reserve v,u for VECTOR of RLSp_AlmostZeroFunct M;

theorem
f=v & g=u implies f+g=v+u
proof
   assume A1: f=v & g=u;
   reconsider v2=v, u2=u as VECTOR of RLSp_L1Funct M by TARSKI:def 3;
   thus v+u=v2+u2 by RLSUB121 .=f+g by ThB10,A1;
end;

theorem
f=u implies a(#)f=a*u
proof
   assume A1: f=u;
   reconsider u2=u as VECTOR of RLSp_L1Funct M by TARSKI:def 3;
   thus a*u=a*u2 by RLSUB122 .=a(#)f by ThB11,A1;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
      f be PartFunc of X,REAL;
  func a.e-eq-class(f,M) -> Subset of L1_Functions M equals
  {g where g is PartFunc of X,REAL :
   g in L1_Functions M & f in L1_Functions M & f a.e.= g,M };
correctness
proof
   now let x be set;
    assume x in {g where g is PartFunc of X,REAL :
                  g in L1_Functions M &
                  f in L1_Functions M & f a.e.= g,M }; then
    ex g be PartFunc of X,REAL st x=g & g in L1_Functions M &
     f in L1_Functions M & f a.e.= g,M;
    hence x in L1_Functions M;
   end;
   hence thesis by TARSKI:def 3;
end;
end;

theorem EQC00:
f in L1_Functions M & g in L1_Functions M implies
 (g a.e.= f,M iff g in a.e-eq-class(f,M))
proof
   assume
A1: f in L1_Functions M & g in L1_Functions M;
   hereby assume g a.e.= f,M; then
    f a.e.= g,M by Th05;
    hence g in a.e-eq-class(f,M) by A1;
   end;
   hereby assume g in a.e-eq-class(f,M); then
    ex r be PartFunc of X,REAL st g=r & r in L1_Functions M &
      f in L1_Functions M & f a.e.= r,M;
    hence g a.e.= f,M by Th05;
   end;
end;

theorem EQC01:
f in L1_Functions M implies f in a.e-eq-class(f,M)
proof
   hereby assume A1: f in L1_Functions M;
    f a.e.= f,M by Th04;
    hence f in a.e-eq-class(f,M) by A1;
   end;
end;

theorem EQC02:
f in L1_Functions M & g in L1_Functions M implies
  (a.e-eq-class(f,M) = a.e-eq-class(g,M) iff f a.e.= g,M)
proof
   assume A0:f in L1_Functions M & g in L1_Functions M;
   hereby assume a.e-eq-class(f,M) = a.e-eq-class(g,M); then
    f in {r where r is PartFunc of X,REAL : r in L1_Functions M &
           g in L1_Functions M & g a.e.= r,M } by A0,EQC01; then
    ex r be PartFunc of X,REAL st
      f=r & r in L1_Functions M &
      g in L1_Functions M & g a.e.= r,M;
    hence f a.e.= g,M by Th05;
   end;
   assume A2: f a.e.= g,M;
   now let x be set;
    assume x in a.e-eq-class(f,M); then
    consider r be PartFunc of X,REAL such that
A3:  x=r & r in L1_Functions M &
     f in L1_Functions M & f a.e.= r,M;
    g a.e.= f,M by Th05,A2; then
    g a.e.= r,M by Th06,A3;
    hence x in a.e-eq-class(g,M) by A0,A3;
   end; then
A4:a.e-eq-class(f,M) c= a.e-eq-class(g,M) by TARSKI:def 3;
   now let x be set;
    assume x in a.e-eq-class(g,M); then
    consider r be PartFunc of X,REAL such that
A5:  x=r & r in L1_Functions M &
     g in L1_Functions M & g a.e.= r,M;
    f a.e.= r,M by A2,A5,Th06;
    hence x in a.e-eq-class(f,M) by A0,A5;
   end; then
   a.e-eq-class(g,M) c= a.e-eq-class(f,M) by TARSKI:def 3;
   hence a.e-eq-class(f,M) = a.e-eq-class(g,M) by A4,XBOOLE_0:def 10;
end;

theorem
f in L1_Functions M & g in L1_Functions M implies
  (a.e-eq-class(f,M) = a.e-eq-class(g,M) iff g in a.e-eq-class(f,M))
proof
   assume
A1: f in L1_Functions M & g in L1_Functions M; then
   g a.e.= f,M iff g in a.e-eq-class(f,M) by EQC00;
   hence thesis by A1,EQC02;
end;

theorem EQC03:
f in L1_Functions M & f1 in L1_Functions M &
g in L1_Functions M & g1 in L1_Functions M &
a.e-eq-class(f,M) = a.e-eq-class(f1,M) & a.e-eq-class(g,M) = a.e-eq-class(g1,M)
implies a.e-eq-class(f+g,M) = a.e-eq-class(f1+g1,M)
proof
   assume
A1:f in L1_Functions M & f1 in L1_Functions M &
   g in L1_Functions M & g1 in L1_Functions M &
   a.e-eq-class(f,M) = a.e-eq-class(f1,M) &
   a.e-eq-class(g,M) = a.e-eq-class(g1,M); then
   f a.e.= f1,M & g a.e.= g1,M by EQC02; then
   f + g in L1_Functions M & f1+g1 in L1_Functions M &
   f + g a.e.= f1+g1,M by A1,Th01a,Th07;
   hence thesis by EQC02;
end;

theorem EQC04:
f in L1_Functions M & g in L1_Functions M &
a.e-eq-class(f,M) = a.e-eq-class(g,M) implies
  a.e-eq-class(a(#)f,M) = a.e-eq-class(a(#)g,M)
proof
   assume
A1: f in L1_Functions M & g in L1_Functions M &
    a.e-eq-class(f,M) = a.e-eq-class(g,M); then
   f a.e.= g ,M & f in L1_Functions M &
   g in L1_Functions M by EQC02; then
A2:a(#)f a.e.= a(#)g,M by Th08;
   a(#)f in L1_Functions M &
   a(#)g in L1_Functions M by A1,Th01b;
   hence thesis by A2,EQC02;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  func CosetSet M -> non empty Subset-Family of L1_Functions M equals
    {a.e-eq-class(f,M) where f is PartFunc of X,REAL :
      f in L1_Functions M};
correctness
proof
   set C = {a.e-eq-class(f,M) where f is PartFunc of X,REAL :
             f in L1_Functions M};
A1:C c= bool L1_Functions M
   proof
    let x be set;assume x in C; then
    ex f be PartFunc of X,REAL st
     a.e-eq-class(f,M) = x & f in L1_Functions M;
    hence x in bool L1_Functions M;
   end;
   X-->0 in L1_Functions M by LmDef1; then
   a.e-eq-class(X-->0,M) in C;
   hence thesis by A1;
end;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  func addCoset M -> BinOp of CosetSet M means :VSPDef3X:
    for A,B be Element of CosetSet M, a,b be PartFunc of X,REAL st
      a in A & b in B holds it.(A,B) = a.e-eq-class(a+b,M);
existence
proof
   set C = CosetSet M;
   defpred P[set,set,set] means
    for a,b be PartFunc of X,REAL st a in  $1&  b in $2 holds
      $3 = a.e-eq-class(a+b,M);
A1:now let A,B be Element of C;
    A in C; then
    consider a be PartFunc of X,REAL such that
A2:  A=a.e-eq-class(a,M) & a in L1_Functions M;
    B in C; then
    consider b be PartFunc of X,REAL such that
A3:  B=a.e-eq-class(b,M) & b in L1_Functions M;
    set z = a.e-eq-class(a+b,M);
A4: a+b is PartFunc of X,REAL & a+b in L1_Functions M by Th01a,A2,A3; then
    z in C; then
    reconsider z as Element of C;
    take z;
    now let a1,b1 be PartFunc of X,REAL;
     assume A5: a1 in A & b1 in B; then
     a1 a.e.= a,M & b1 a.e.= b,M by A2,A3,EQC00; then
A6:  a1+b1 a.e.= a+b,M by Th07;
     a1+b1 is PartFunc of X,REAL & a1+b1 in L1_Functions M by A5,Th01a;
     hence z = a.e-eq-class(a1+b1,M) by EQC02,A4,A6;
    end;
    hence P[A,B,z];
   end;
   consider f be Function of [:C,C:],C such that
A8: for A,B be Element of C holds P[A,B, f.(A,B)] from BINOP_1:sch 3(A1);
   reconsider f as BinOp of C;
   take f;
   let A,B be Element of C;
   let a,b be PartFunc of X,REAL;
   assume a in A  & b in B;
   hence f.(A,B) = a.e-eq-class(a+b,M) by A8;
end;
uniqueness
proof
   let f1,f2 be BinOp of CosetSet M such that
A9: for A,B be Element of CosetSet M, a,b be PartFunc of X,REAL st
      a in A & b in B holds f1.(A,B) = a.e-eq-class(a+b,M) and
A10:for A,B be Element of CosetSet M, a,b be PartFunc of X,REAL st
      a in A & b in B holds f2.(A,B) = a.e-eq-class(a+b,M);
   set C = CosetSet M;
   now let A,B be Element of CosetSet M;
    A in C; then
    consider a1 be PartFunc of X,REAL such that
A11: A=a.e-eq-class(a1,M) & a1 in L1_Functions M;
    B in C; then
    consider b1 be PartFunc of X,REAL such that
A12: B=a.e-eq-class(b1,M) & b1 in L1_Functions M;
A13:a1 in A & b1 in B by A11,A12,EQC01; then
    f1.(A,B) = a.e-eq-class(a1+b1,M) by A9;
    hence f1.(A,B) = f2.(A,B) by A10,A13;
   end;
   hence thesis by BINOP_1:2;
end;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  func zeroCoset M -> Element of CosetSet M means :VSPDef4X:
    ex f be PartFunc of X,REAL st f = X --> 0 & f in L1_Functions M &
      it = a.e-eq-class(f,M);
correctness
proof
   X-->0 in L1_Functions M by LmDef1; then
   a.e-eq-class(X-->0,M) in CosetSet M;
   hence thesis by LmDef1;
end;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  func lmultCoset M -> Function of [:REAL, CosetSet M:],CosetSet M means
 :VSPDef5X:
  for z be Element of REAL, A be Element of CosetSet M,
      f be PartFunc of X,REAL st
   f in A holds it.(z,A) = a.e-eq-class(z(#)f,M);
existence
proof
   set C = CosetSet M;
   defpred P[Element of REAL,set,set] means
     for f be PartFunc of X,REAL st f in $2 holds $3 = a.e-eq-class($1(#)f,M);
A1:now let z be Element of REAL, A be Element of C;
    A in C; then
    consider a be PartFunc of X,REAL such that
A2:  A = a.e-eq-class(a,M) & a in L1_Functions M;
    set c = a.e-eq-class(z(#)a,M);
A3: z(#)a is PartFunc of X,REAL & z(#)a in L1_Functions M by Th01b,A2; then
    c in C; then
    reconsider c as Element of C;
    take c;
    now let a1 be PartFunc of X,REAL;
     assume A4: a1 in A; then
     a1 a.e.= a,M by A2,EQC00; then
A5:  z(#)a1 a.e.= z(#)a,M by Th08;
     z(#)a1 is PartFunc of X,REAL & z(#)a1 in L1_Functions M by Th01b,A4;
     hence c = a.e-eq-class(z(#)a1,M) by EQC02,A3,A5;
    end;
    hence P[z,A,c];
   end;
   consider f be Function of [:REAL,C:],C such that
A7: for z be Element of REAL, A be Element of C holds P[z,A, f.(z,A)]
      from BINOP_1:sch 3(A1);
   take f;
   let z be Element of REAL, A be Element of C, a be PartFunc of X,REAL;
   assume a in A;
   hence f.(z,A) = a.e-eq-class(z(#)a,M) by A7;
end;
uniqueness
proof
   set C = CosetSet M;
   let f1,f2 be Function of [:REAL,C:],C such that
A8: for z be Element of REAL, A be Element of CosetSet M,
     a be PartFunc of X,REAL st a in A holds
     f1.(z,A) = a.e-eq-class(z(#)a,M) and
A9: for z be Element of REAL, A be Element of CosetSet M,
     a be PartFunc of X,REAL st a in A holds
     f2.(z,A) = a.e-eq-class(z(#)a,M);
   now let z be Element of REAL, A be Element of CosetSet M;
    A in C; then
    consider a1 be PartFunc of X,REAL such that
A10: A=a.e-eq-class(a1,M) & a1 in L1_Functions M;
    thus f1.(z,A) = a.e-eq-class(z(#)a1,M) by A8,A10,EQC01
                 .= f2.(z,A) by A9,A10,EQC01;
   end;
   hence thesis by BINOP_1:2;
end;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  func Pre-L-Space M -> strict Abelian add-associative right_zeroed
                      right_complementable RealLinearSpace-like
                      (non empty RLSStruct) means :VSPDef6X:
  the carrier of it = CosetSet M &
  the addF of it = addCoset M &
  0.it = zeroCoset M &
  the Mult of it = lmultCoset M;
existence
proof
   set C = CosetSet M, aC = addCoset M, zC = zeroCoset M,
      lC = lmultCoset M, A = RLSStruct (# C,zC,aC,lC #);
A1:A is Abelian
   proof
    let A1,A2 be Element of A;
    A1 in C; then
    consider a be PartFunc of X,REAL such that
A2:  A1 = a.e-eq-class(a,M) & a in L1_Functions M;
    A2 in C; then
    consider b be PartFunc of X,REAL such that
A4:  A2 = a.e-eq-class(b,M) & b in L1_Functions M;
A3: a in A1 & b in A2 by A2,A4,EQC01; then
    A1+A2 = a.e-eq-class(a+b,M) by VSPDef3X;
    hence A1+A2 = A2+A1 by A3,VSPDef3X;
   end;
A6:A is add-associative
   proof
    let A1,A2,A3 be Element of A;
    A1 in C; then
    consider a be PartFunc of X,REAL such that
A7:  A1=a.e-eq-class(a,M) & a in L1_Functions M;
    A2 in C; then
    consider b be PartFunc of X,REAL such that
A9:  A2=a.e-eq-class(b,M) & b in L1_Functions M;
    A3 in C; then
    consider c be PartFunc of X,REAL such that
A11: A3=a.e-eq-class(c,M) & c in L1_Functions M;
A8: a in A1 & b in A2 & c in A3 by A7,A9,A11,EQC01; then
    aC.(A1,A2) =a.e-eq-class(a+b,M) &
    aC.(A2,A3) =a.e-eq-class(b+c,M) by VSPDef3X; then
A15:a+b in A1+A2 & b+c in A2+A3 by EQC01,Th01a,A7,A9,A11;
    reconsider a1=a,b1=b,c1=c as VECTOR of RLSp_L1Funct M by A7,A9,A11;
A17:a+b = a1+b1 & b+c = b1+c1 by ThB10; then
    a+(b+c) =a1+(b1+c1) by ThB10; then
    a+(b+c) =(a1+b1)+c1 by RLVECT_1:def 6; then
    a+(b+c) = a+b+c by A17,ThB10; then
    A1+A2+A3 = a.e-eq-class(a+(b+c),M) by A8,A15,VSPDef3X;
    hence A1+A2+A3 = A1+(A2+A3) by A8,A15,VSPDef3X;
   end;

A19: A is right_zeroed
   proof
    let A1 be Element of A;
    A1 in C; then
    consider a be PartFunc of X,REAL such that
A20: A1=a.e-eq-class(a,M) & a in L1_Functions M;
A21:a in A1 by A20,EQC01;
    reconsider a1=a as VECTOR of RLSp_L1Funct M by A20;
    consider z be PartFunc of X,REAL such that
A22: z = X --> 0 & z in L1_Functions M &
     zeroCoset M=a.e-eq-class(z,M) by VSPDef4X;
A23:z in 0.A by A22,EQC01;
    reconsider a1=a,z1=z as VECTOR of
        RLSp_L1Funct M by A20,A22;
    a+z =a1+z1 by ThB10
       .=a1+0.RLSp_L1Funct M by Th09a,A22
       .=a by RLVECT_1:def 7;
    hence A1+0.A = A1 by A20,A21,A23,VSPDef3X;
   end;
A25: A is right_complementable
   proof
    let A1 be Element of A;
    A1 in C; then
    consider a be PartFunc of X,REAL such that
A26: A1=a.e-eq-class(a,M) & a in L1_Functions M;
A27:a in A1 by A26,EQC01;
    reconsider a1=a as VECTOR of RLSp_L1Funct M by A26;
A28:(-1)(#)a in L1_Functions M by A26,Th01b;
    set A2 = a.e-eq-class((-1)(#)a,M);
    A2 in C by A28; then
    reconsider A2 as Element of A;
    take A2;
A29:(-1)(#)a in A2 by EQC01,A26,Th01b;
    consider v,g be PartFunc of X,REAL such that
A30: v in L1_Functions M & g in L1_Functions M &
     v = a1+(-1)*a1 & g = X --> 0 & v a.e.= g,M by ThB11Z;
    (-1)(#)a = (-1)*a1 by ThB11; then
A31:a+(-1)(#)a a.e.= g,M by ThB10,A30;
A32:a+(-1)(#)a in L1_Functions M by Th01a,A26,A28;
    ex z be PartFunc of X,REAL st z = X --> 0 & z in L1_Functions M &
     zeroCoset M=a.e-eq-class(z,M) by VSPDef4X; then
    0.A = a.e-eq-class(a+ (-1)(#)a,M) by A31,EQC02,A30,A32;
    hence A1 + A2 = 0.A by A27,A29,VSPDef3X;
   end;
   now let x,y be Element of REAL, A1,A2 be Element of A;
    A1 in C; then
    consider a be PartFunc of X,REAL such that
A35: A1=a.e-eq-class(a,M) & a in L1_Functions M;
    A2 in C; then
    consider b be PartFunc of X,REAL such that
A37: A2=a.e-eq-class(b,M) & b in L1_Functions M;
A36:a in A1 & b in A2 by A35,A37,EQC01; then
    aC.(A1,A2) =a.e-eq-class(a+b,M) by VSPDef3X; then
A40:a+b in (A1+A2) by EQC01,Th01a,A35,A37;
A41:lC.(x,A1) =a.e-eq-class(x(#)a,M) by A36,VSPDef5X;
    reconsider a1=a,b1=b as VECTOR of RLSp_L1Funct M by A35,A37;
A42:y(#)a = y*a1 & x(#)a = x*a1 & x(#)b = x*b1 by ThB11;
    a+b = a1+b1 by ThB10; then
    x(#)(a+b) = x*(a1+b1) by ThB11; then
    x(#)(a+b) = x*a1+x*b1 by RLVECT_1:def 9; then
A45:x(#)(a+b) = x(#)a + x(#)b by A42,ThB10;
A46:(x+y)(#)a = (x+y)*a1 by ThB11 .= x*a1+y*a1 by RLVECT_1:def 9
     .= x(#)a + y(#)a by A42,ThB10;
A47:1(#)a =1*a1 by ThB11 .= a by RLVECT_1:def 9;
A48:x(#)(y(#)a) =x*(y*a1) by A42,ThB11 .= (x*y)*a1 by RLVECT_1:def 9
     .= (x*y)(#)a by ThB11;
A49:x(#)a in x*A1 by EQC01,A41,Th01b,A35;
    lC.(x,A2) =a.e-eq-class(x(#)b,M) by A36,VSPDef5X; then
A51:x(#)b in x*A2 by EQC01,Th01b,A37;
    x*(A1+A2) = a.e-eq-class(x(#)a+x(#)b,M) by A45,A40,VSPDef5X;
    hence x*(A1+A2) = x*A1+x*A2 by A49,A51,VSPDef3X;
    lC.(y,A1) =a.e-eq-class(y(#)a,M) by A36,VSPDef5X; then
A53:y(#)a in y*A1 by EQC01,Th01b,A35;
    (x+y)*A1 = a.e-eq-class(x(#)a+y(#)a,M) by A46,A36,VSPDef5X;
    hence (x+y)*A1 = x*A1+y*A1 by A49,A53,VSPDef3X;
    thus (x*y)*A1 = a.e-eq-class(x(#)(y(#)a),M) by A48,A36,VSPDef5X
      .=x*(y*A1) by A53,VSPDef5X;
    thus 1*A1 = A1 by A35,A47,A36,VSPDef5X;
   end; then
   reconsider A as strict Abelian add-associative right_zeroed
     right_complementable RealLinearSpace-like (non empty RLSStruct)
     by A1,A6,A19,A25,RLVECT_1:def 9;
   take A;
   thus thesis;
end;
uniqueness;
end;

begin :: Real Normed Space of Integrable Functions

theorem Th14a:
f in L1_Functions M & g in L1_Functions M & f a.e.= g,M implies
  Integral(M,f) = Integral(M,g)
proof
   assume
A1: f in L1_Functions M & g in L1_Functions M & f a.e.= g,M;
A2:ex f1 be PartFunc of X,REAL st
    f=f1 & ex ND be Element of S st M.ND=0 & dom f1 = ND` &
    f1 is_integrable_on M by A1; then
   consider NDf be Element of S such that
A3: M.NDf=0 & dom f = NDf` & f is_integrable_on M;
A4:ex g1 be PartFunc of X,REAL st
    g=g1 & ex ND be Element of S st M.ND=0 & dom g1 = ND` &
    g1 is_integrable_on M by A1; then
   consider NDg be Element of S such that
A5: M.NDg=0 & dom g = NDg` & g is_integrable_on M;
   consider EQ being Element of S such that
A6: M.EQ = 0 & f|EQ` = g|EQ` by A1,Def2;
   R_EAL f is_integrable_on M by A2,MESFUNC6:def 9; then
   consider E1 being Element of S such that
A7: E1 = dom R_EAL f & R_EAL f is_measurable_on E1 by MESFUNC5:def 17;
A8:E1 = dom f & f is_measurable_on E1 by A7,MESFUNC6:def 6;
   R_EAL g is_integrable_on M by A4,MESFUNC6:def 9; then
   consider E2 being Element of S such that
A9: E2 = dom R_EAL g & R_EAL g is_measurable_on E2 by MESFUNC5:def 17;
A10:E2 = dom g & g is_measurable_on E2 by A9,MESFUNC6:def 6;
A11: EQ` \ (NDf \/NDg) = (EQ \/ (NDf \/NDg))` by XBOOLE_1:41
     .= (NDf \/ (EQ \/NDg))` by XBOOLE_1:4
     .= NDf` \ (EQ \/NDg) by XBOOLE_1:41;
A12:EQ` \ (NDf \/NDg) = (EQ \/ (NDf \/NDg))` by XBOOLE_1:41
     .=(NDg \/ (EQ \/NDf))` by XBOOLE_1:4
     .=NDg` \ (EQ \/NDf) by XBOOLE_1:41;
A13: EQ` \ (NDf \/NDg) c= EQ` by XBOOLE_1:36; then
A14: f|(EQ` \ (NDf \/NDg)) = g|EQ`|(EQ`\(NDf \/NDg)) by A6,FUNCT_1:82
    .= g|(EQ`\(NDf \/ NDg)) by A13,FUNCT_1:82;
A17:M.(EQ \/ NDf) = 0 by A3,A6,MLm01;
   M.(EQ \/ NDg) = 0 by A5,A6,MLm01;
   hence Integral(M,f) = Integral(M,g|(NDg` \(EQ\/NDf)))
             by A3,A8,A11,A12,A14,MESFUNC6:89
         .= Integral(M,g) by A5,A10,A17,MESFUNC6:89;
end;

theorem Lm15:
f is_integrable_on M implies
  Integral(M,f) in REAL & Integral(M,abs f) in REAL &
  abs f is_integrable_on M
proof
   assume A1: f is_integrable_on M; then
A2:-infty < Integral(M,f) & Integral(M,f) < +infty by MESFUNC6:90;
   R_EAL f is_integrable_on M by A1,MESFUNC6:def 9; then
   consider A be Element of S such that
A3: A = dom R_EAL f & R_EAL f is_measurable_on A by MESFUNC5:def 17;
A4:A = dom f & f is_measurable_on A by A3,MESFUNC6:def 6; then
   abs f is_integrable_on M by A1,MESFUNC6:94; then
   -infty < Integral(M,abs f) & Integral(M,abs f) < +infty by MESFUNC6:90;
   hence thesis by A1,A2,A4,MESFUNC6:94,XXREAL_0:14;
end;

theorem Th14:
f in L1_Functions M & g in L1_Functions M & f a.e.= g,M implies
  abs f a.e.= (abs g),M & Integral(M,abs f) = Integral(M,abs g)
proof
   assume that
A1: f in L1_Functions M & g in L1_Functions M & f a.e.= g,M;
A2:ex f1 be PartFunc of X,REAL st
    f=f1 & ex ND be Element of S st M.ND=0 & dom f1 = ND` &
    f1 is_integrable_on M by A1; then
   consider NDf be Element of S such that
A3: M.NDf=0 & dom f = NDf` & f is_integrable_on M;
A4:ex g1 be PartFunc of X,REAL st
    g=g1 & ex ND be Element of S st M.ND=0 & dom g1 = ND` &
    g1 is_integrable_on M by A1; then
   consider NDg be Element of S such that
A5: M.NDg=0 & dom g = NDg` & g is_integrable_on M;
   consider EQ being Element of S such that
A6: M.EQ = 0 & f|EQ` = g|EQ` by A1,Def2;
A8:abs f is_integrable_on M & abs g is_integrable_on M by A2,A4,Lm15;
   dom abs f = NDf` & dom abs g = NDg` by A3,A5,VALUED_1:def 11; then
A9:abs f in L1_Functions M & abs g in L1_Functions M by A3,A5,A8;
   (abs f)|EQ` = abs(g|EQ`) by A6,RFUNCT_1:62
     .= (abs g)|EQ` by RFUNCT_1:62; then
   abs f a.e.= (abs g),M by Def2,A6;
   hence thesis by A9,Th14a;
end;

theorem Lm10:
(ex x be VECTOR of Pre-L-Space M st f in x & g in x) implies
  f a.e.= g,M & f in L1_Functions M & g in L1_Functions M
proof
   assume ex x be VECTOR of Pre-L-Space M st f in x & g in x; then
   consider x be VECTOR of Pre-L-Space M such that
A1: f in x & g in x;
   x in the carrier of Pre-L-Space M; then
   x in CosetSet M by VSPDef6X; then
   consider h be PartFunc of X,REAL such that
A2: x=a.e-eq-class(h,M) & h in L1_Functions M;
A4:ex k be PartFunc of X,REAL st f=k & k in L1_Functions M &
     h in L1_Functions M & h a.e.= k,M by A1,A2;
   ex j be PartFunc of X,REAL st g=j & j in L1_Functions M &
     h in L1_Functions M & h a.e.= j,M by A1,A2; then
   f a.e.= h,M & h a.e.= g,M by A4,Th05;
   hence thesis by A1,A2,Th06;
end;

theorem Th15:
ex NORM be Function of the carrier of Pre-L-Space M,REAL st
  for x be Point of Pre-L-Space M
    ex f be PartFunc of X,REAL st f in x & NORM.x = Integral(M,abs f)
proof
   defpred P[set,set] means
     ex f be PartFunc of X,REAL st f in $1 & $2 = Integral(M,abs f);
A1:for x be Point of Pre-L-Space M ex y being Element of REAL st P[x,y]
   proof
    let x be Point of Pre-L-Space M;
    x in the carrier of Pre-L-Space M; then
    x in CosetSet M by VSPDef6X; then
    consider f be PartFunc of X,REAL such that
A2:  x=a.e-eq-class(f,M) & f in L1_Functions M;
    ex f0 be PartFunc of X,REAL st
     f=f0 & ex ND be Element of S st M.ND=0 & dom f0 = ND` &
     f0 is_integrable_on M by A2; then
    Integral(M,abs f) in REAL by Lm15;
    hence thesis by A2,EQC01;
   end;
   consider f being Function of Pre-L-Space M,REAL such that
A5: for x being Point of Pre-L-Space M holds P[x,f.x] from FUNCT_2:sch 3(A1);
   take f;
   thus thesis by A5;
end;

reserve x for Point of Pre-L-Space M;

theorem Lm16:
f in x implies
  f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M
proof
   assume A1: f in x;
   x in the carrier of Pre-L-Space M; then
   x in CosetSet M by VSPDef6X; then
   consider h be PartFunc of X,REAL such that
A2: x=a.e-eq-class(h,M) & h in L1_Functions M;
   ex g be PartFunc of X,REAL st
    f=g & g in L1_Functions M &
    h in L1_Functions M & h a.e.= g,M by A1,A2; then
   ex f0 be PartFunc of X,REAL st
    f=f0 & ex ND be Element of S st M.ND=0 & dom f0 = ND` &
    f0 is_integrable_on M;
   hence thesis by Lm15;
end;

theorem Lm17:
f in x & g in x implies
  f a.e.= g,M & Integral(M,f) = Integral(M,g) &
  Integral(M,abs f) = Integral(M,abs g)
proof
   assume f in x & g in x; then
   f a.e.= g,M & f in L1_Functions M & g in L1_Functions M by Lm10;
   hence thesis by Th14,Th14a;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func L-1-Norm M -> Function of the carrier of Pre-L-Space M,REAL means :Def20:
 for x be Point of Pre-L-Space M
  ex f be PartFunc of X,REAL st f in x & it.x = Integral(M,abs f);
existence by Th15;
uniqueness
proof
   let N1,N2 be Function of the carrier of Pre-L-Space M,REAL;
   assume
A1: (for x be Point of Pre-L-Space M ex f be PartFunc of X,REAL st
       f in x & N1.x = Integral(M,abs f)) &
    (for x be Point of Pre-L-Space M ex g be PartFunc of X,REAL st
       g in x & N2.x = Integral(M,abs g));
   now let x be Point of Pre-L-Space M;
    (ex f be PartFunc of X,REAL st f in x & N1.x = Integral(M,abs f)) &
    ex g be PartFunc of X,REAL st g in x & N2.x = Integral(M,abs g) by A1;
    hence N1.x=N2.x by Lm17;
   end;
   hence N1=N2 by FUNCT_2:113;
end;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  func L-1-Space M -> non empty NORMSTR equals
    NORMSTR (# the carrier of Pre-L-Space M, the ZeroF of Pre-L-Space M,
               the addF of Pre-L-Space M, the Mult of Pre-L-Space M,
               L-1-Norm M #);
  coherence;
end;

reserve x,y for Point of L-1-Space M;

theorem Lm17x:
( ex f be PartFunc of X,REAL st f in L1_Functions M &
    x= a.e-eq-class(f,M) & ||.x.|| = Integral(M,abs f) ) &
 for f be PartFunc of X,REAL st f in x holds Integral(M,abs f) = ||.x.||
proof
   reconsider y=x as Point of Pre-L-Space M;
   consider f be PartFunc of X,REAL such that
A1: f in y & (L-1-Norm M).y = Integral(M,abs f) by Def20;
   y in the carrier of Pre-L-Space M; then
   y in CosetSet M by VSPDef6X; then
   consider g be PartFunc of X,REAL such that
A2: y=a.e-eq-class(g,M) & g in L1_Functions M;
   g in y by A2,EQC01; then
   f a.e.= g,M & f in L1_Functions M & g in L1_Functions M by A1,Lm10; then
   x = a.e-eq-class(f,M) by EQC02,A2;
   hence thesis by A1,Lm17;
end;

theorem Lm17z:
f in x implies x= a.e-eq-class(f,M) & ||.x.|| = Integral(M,abs f)
proof
   assume A1:f in x;
   reconsider y=x as Point of Pre-L-Space M;
   y in the carrier of Pre-L-Space M; then
   y in CosetSet M by VSPDef6X; then
   consider g be PartFunc of X,REAL such that
A2: y=a.e-eq-class(g,M) & g in L1_Functions M;
   g in y by A2,EQC01; then
   f a.e.= g,M & f in L1_Functions M & g in L1_Functions M by A1,Lm10;
   hence thesis by Lm17x,A1,A2,EQC02;
end;

theorem Lm17Y:
(f in x & g in y implies f+g in x+y) &
(f in x implies a(#)f in a*x)
proof
   set C = CosetSet M;
   hereby assume A2: f in x & g in y;
    reconsider x1=x,y1=y as Point of Pre-L-Space M;
    x1 in the carrier of Pre-L-Space M; then
A3: x1 in C by VSPDef6X; then
    consider a be PartFunc of X,REAL such that
A4:  x1=a.e-eq-class(a,M) & a in L1_Functions M;
A5: a in x1 by A4,EQC01;
    y1 in the carrier of Pre-L-Space M; then
A6: y1 in C by VSPDef6X; then
    consider b be PartFunc of X,REAL such that
A7:  y1=a.e-eq-class(b,M) & b in L1_Functions M;
    b in y1 by A7,EQC01; then
    (addCoset M).(x1,y1) = a.e-eq-class(a+b,M) by A3,A6,A5,VSPDef3X; then
A9: x1+y1 = a.e-eq-class(a+b,M) by VSPDef6X;
    ex r be PartFunc of X,REAL st f=r & r in L1_Functions M &
      a in L1_Functions M & a a.e.= r,M by A2,A4; then
A11:a.e-eq-class(a,M) = a.e-eq-class(f,M) by EQC02;
    ex r be PartFunc of X,REAL st g=r & r in L1_Functions M &
      b in L1_Functions M & b a.e.= r,M by A2,A7; then
    a.e-eq-class(b,M) = a.e-eq-class(g,M) by EQC02; then
    a.e-eq-class(a+b,M) = a.e-eq-class(f+g,M) by A2,A4,A7,A11,EQC03;
    hence f+g in x+y by EQC01,A9,Th01a,A4,A2,A7;
   end;
   hereby
    assume A15:f in x;
    reconsider x1=x as Point of Pre-L-Space M;
    x1 in the carrier of Pre-L-Space M; then
A16:x1 in C by VSPDef6X; then
    consider f1 be PartFunc of X,REAL such that
A17: x1=a.e-eq-class(f1,M) & f1 in L1_Functions M;
    f1 in x1 by A17,EQC01; then
    (lmultCoset M).(a,x1) = a.e-eq-class(a(#)f1,M) by A16,VSPDef5X; then
A19:a*x1 = a.e-eq-class(a(#)f1,M) by VSPDef6X;
    ex r be PartFunc of X,REAL st f=r & r in L1_Functions M &
      f1 in L1_Functions M & f1 a.e.= r,M by A15,A17; then
    a.e-eq-class(f1,M) = a.e-eq-class(f,M) by EQC02; then
    a.e-eq-class(a(#)f1,M) = a.e-eq-class(a(#)f,M) by A17,A15,EQC04;
    hence a(#)f in a*x by A19,Th01b,A15,A17,EQC01;
   end;
end;

theorem Lm261a:
E = dom f & (for x be set st x in dom f holds f.x=r)
  implies f is_measurable_on E
proof
   assume A1: E = dom f;
   assume A2: for x be set st x in dom f holds f.x=r;
   set g=R_EAL f;
   r in REAL; then
   reconsider r0=r as R_eal by NUMBERS:31;
   consider g0 be PartFunc of X,ExtREAL such that
A3: g0 is_simple_func_in S & dom g0 = E &
    (for x be set st x in E holds g0.x=r0) by MESFUNC5:47;
   now let x be Element of X;
    assume A4: x in dom g; then
    g.x = r by A2;
    hence g.x = g0.x by A1,A3,A4;
   end; then
   g0=g by A1,A3,PARTFUN1:34; then
   g is_measurable_on E by A3,MESFUNC2:37;
   hence f is_measurable_on E by MESFUNC6:def 6;
end;

theorem Lm261:
f in L1_Functions M & Integral(M,abs f) = 0 implies
   f a.e.= X-->0,M
proof
   assume
A1: f in L1_Functions M & Integral(M,abs f) = 0; then
   consider f1 be PartFunc of X,REAL such that
A2: f=f1 & ex ND be Element of S st M.ND=0 & dom f1 = ND` &
    f1 is_integrable_on M;
   consider ND be Element of S such that
A3: M.ND=0 & dom f1 = ND` & f1 is_integrable_on M by A2;
A4:abs f is_integrable_on M by Lm15,A2; then
   R_EAL abs f is_integrable_on M by MESFUNC6:def 9; then
   consider E be Element of S such that
A5: E = dom R_EAL abs f & R_EAL abs f is_measurable_on E by MESFUNC5:def 17;
A6:E = dom abs f & abs f is_measurable_on E by A5,MESFUNC6:def 6;
   now let x be set;
    assume x in dom abs f; then
    (abs f).x = abs(f.x) by VALUED_1:def 11;
    hence 0 <= (abs f).x by COMPLEX1:132;
   end; then
A7:abs f is nonnegative by MESFUNC6:52;
   defpred P[Element of NAT,set] means
     $2=great_eq_dom(abs f,1/($1+1)) & M.($2)=0;
A8:now let n be Element of NAT;
    set r=1/(n+1);
    reconsider Br=E /\ great_eq_dom(abs f,r) as Element of S by A6,MESFUNC6:13;
A9: Integral(M,(abs f)|Br) <= Integral(M,(abs f)|E)
      by A6,A7,MESFUNC6:87,XBOOLE_1:17;
    set g = Br --> r;
A10:dom g = Br by FUNCT_2:def 1;
A11:for x be set st x in dom g holds g.x = r by FUNCOP_1:13;
    reconsider g as PartFunc of X,REAL by PARTFUN1:30;
A12:g is_measurable_on Br by A10,A11,Lm261a;
    for x be set st x in dom g holds 0 <= g.x by A11; then
A13:g is nonnegative by MESFUNC6:52;
    dom ((abs f)|Br) = dom (abs f) /\ Br by RELAT_1:90
      .= Br by A5,XBOOLE_1:17,28; then
A14:dom g = dom ((abs f)|Br) & (abs f)|Br is_integrable_on M
      by A4,FUNCT_2:def 1,MESFUNC6:91;
    for x be set st x in great_eq_dom(abs f,r) holds x in dom abs f
      by MESFUNC6:6; then
A15:great_eq_dom(abs f,r) c= E by A5,TARSKI:def 3;
    now let x be Element of X;
     assume A16: x in dom g; then
     abs(g.x) = abs r by A11; then
A17: abs(g.x) = r by ABSVALUE:def 1;
     x in E /\ great_eq_dom(abs f,r) by A16,FUNCT_2:def 1; then
     x in great_eq_dom(abs f,r) by XBOOLE_0:def 4; then
     ex y being Real st y=(abs f).x & r <= y by MESFUNC6:6;
     hence abs(g.x) <= ((abs f)|Br).x by A14,A16,A17,FUNCT_1:70;
    end; then
A19:Integral(M,abs g) <= Integral(M,(abs f)|Br) by A12,A14,A10,MESFUNC6:96;
A20:dom abs g =dom g by VALUED_1:def 11;
    now let x be Element of X;
     assume A22: x in dom abs g; then
     (abs g).x = abs(g.x) by VALUED_1:def 11; then
     (abs g).x = abs r by A11,A20,A22; then
     (abs g).x = r by ABSVALUE:def 1;
     hence (abs g).x = g.x by A11,A20,A22;
    end; then
A23:Integral(M, g) <= Integral(M,(abs f)|Br) by A19,A20,PARTFUN1:34;
    0 <= Integral(M,g) by A10,A11,Lm261a,A13,MESFUNC6:84; then
A25:Integral(M,g) = 0 by A9,A5,A1,A23,RELAT_1:97;
    0<= r & dom g in S & r is Real &
    for x be set st x in dom g holds g.x = r by A10,FUNCOP_1:13; then
    R_EAL(r) * M.(Br) =0 by A10,A25,MESFUNC6:97; then
    M.Br =0 by EXTREAL1:22;
    hence ex B be Element of S st P[n,B] by A15,XBOOLE_1:28;
   end;
   consider F be Function of NAT, S such that
A29:for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(A8);
   now let y be set;
    assume y in {x where x is Element of X : x in dom f & f.x <> 0}; then
    consider z be Element of X such that
A32: y=z & z in dom f & f.z <> 0;
A33:z in dom abs f by A32,VALUED_1:def 11; then
    (abs f).z = abs(f.z) by VALUED_1:def 11; then
    0 < (abs f).z by A32,COMPLEX1:133; then
    consider n be Element of NAT such that
A34: 1/(n+1) < (abs f).z - 0 by MESFUNC1:13;
    z in great_eq_dom(abs f,1/(n+1)) by A33,A34,MESFUNC6:6; then
A35:y in F.n by A29,A32;
    F.n in rng F by FUNCT_2:6;
    hence y in union rng F by A35,TARSKI:def 4;
   end; then
A31:{x where x is Element of X : x in dom f & f.x <> 0} c= union rng F
      by TARSKI:def 3;
   now let y be set;
    assume y in union rng F; then
    consider B be set such that
A38: y in B & B in rng F by TARSKI:def 4;
    consider n be set such that
A39: n in NAT & B=F.n by A38,FUNCT_2:17;
    reconsider m=n as Element of NAT by A39;
A40:y in great_eq_dom(abs f,1/(m+1)) by A29,A38,A39; then
A41:y in dom abs f by MESFUNC6:6; then
A46:y in dom f by VALUED_1:def 11;
A43:(abs f).y <> 0 by A40,MESFUNC1:def 15;
    (abs f).y = abs(f.y) by A41,VALUED_1:def 11; then
    f.y <> 0 by A43,ABSVALUE:7;
    hence y in {x where x is Element of X : x in dom f & f.x <> 0} by A46;
   end; then
   union rng F c= {x where x is Element of X : x in dom f & f.x <> 0}
      by TARSKI:def 3; then
A30:{x where x is Element of X : x in dom f & f.x <> 0 } = union rng F
      by A31,XBOOLE_0:def 10;
   now let A be set;
    assume A in rng F; then
    consider n be set such that
A47: n in NAT & A=F.n by FUNCT_2:17;
    reconsider n as Element of NAT by A47;
    M.(F.n) =0 by A29;
    hence A is measure_zero of M by A47,MEASURE1:def 13;
   end; then
A48: union rng F is measure_zero of M by MEASURE2:16;

   reconsider EQ = union rng F \/ ND as Element of S;
   ND is measure_zero of M by A3,MEASURE1:def 13; then
   EQ is measure_zero of M by A48,MEASURE1:70; then
A49: M.EQ=0 by MEASURE1:def 13;

   set g = X-->0;
A51: EQ` = ND` /\ (union rng F)` by XBOOLE_1:53; then
A51a: EQ` c= dom f by A2,A3,XBOOLE_1:17;
A52: dom(f|EQ`) = EQ` by A2,A3,A51,RELAT_1:91,XBOOLE_1:17;
   dom g = X by FUNCOP_1:19; then
A53: dom(g|EQ`) = EQ` by RELAT_1:91;
A54: now let x be set;
    assume A55: x in EQ`; then
    x in (union rng F)` by A51,XBOOLE_0:def 4; then
    not x in union rng F by XBOOLE_0:def 5;
    hence f.x = 0 by A30,A51a,A55;
   end;
   now let y be set;
    assume A57: y in dom(f|EQ`); then
    (f|EQ`).y = f.y by FUNCT_1:70; then
    (f|EQ`).y =0 by A52,A54,A57; then
    (f|EQ`).y =g.y by A57,FUNCOP_1:13;
    hence (f|EQ`).y =(g|EQ`).y by A52,A53,A57,FUNCT_1:70;
   end; then
   f|EQ` = g|EQ` by A51a,A53,FUNCT_1:9,RELAT_1:91;
   hence thesis by Def2,A49;
end;

theorem Lm262:
Integral(M,abs(X-->0)) = 0
proof
   set f=X --> 0;
   dom f = X by FUNCOP_1:19; then
A2:dom abs f = X by VALUED_1:def 11;
   now let x be Element of X;
    assume A3: x in dom abs f;
    f.x = 0 by FUNCOP_1:13; then
    abs (f.x) = 0 by ABSVALUE:7;
    hence (abs f).x = 0 by A3,VALUED_1:def 11;
   end;
   hence Integral(M,abs f) = 0 by Lm2,A2;
end;

theorem Lm263:
f is_integrable_on M & g is_integrable_on M implies
  Integral(M,abs(f+g)) <= Integral(M,abs f) + Integral(M,abs g)
proof
   set f1=R_EAL f; set g1=R_EAL g;
   assume f is_integrable_on M & g is_integrable_on M; then
A1:f1 is_integrable_on M & g1 is_integrable_on M by MESFUNC6:def 9; then
   consider E be Element of S such that
A2: E = dom(f1+g1) & Integral(M,(|.f1+g1.|)|E) <=
     Integral(M,(|.f1.|)|E) + Integral(M,(|.g1.|)|E) by MESFUNC7:22;
   consider B be Element of S such that
A3: B = dom f1 & f1 is_measurable_on B by A1,MESFUNC5:def 17;
   consider C be Element of S such that
A4: C = dom g1 & g1 is_measurable_on C by A1,MESFUNC5:def 17;
A5:B= dom |.f1.| & C= dom |.g1.| by A3,A4,MESFUNC1:def 10;
A7:f1+g1 =R_EAL(f+g) by MESFUNC6:23;
   dom |.f1+g1.| = E by A2,MESFUNC1:def 10; then
   (|.f1+g1.|)|E = |.f1+g1.| by RELAT_1:97; then
A8:Integral(M,(|.f1+g1.|)|E) = Integral(M,|.f+g.|) by A7,MESFUNC6:1;
   E= (dom f1 /\ dom g1)\((f1"{-infty} /\ g1"{+infty}) \/ (f1"{+infty} /\
    g1"{-infty})) by A2,MESFUNC1:def 3; then
   E c= dom f1 & E c= dom g1 by XBOOLE_1:18,36; then
A10: E c= dom |.f1.| & E c= dom |.g1.| by MESFUNC1:def 10;
   |.f1.| is_integrable_on M by A1,A3,MESFUNC5:106; then
   ex E be Element of S st E = dom |.f1.| & |.f1.| is_measurable_on E
    by MESFUNC5:def 17; then
   Integral(M,(|.f1.|)|E) <= Integral(M,(|.f1.|)|B)
     by A5,A10,MESFUNC5:99; then
   Integral(M,(|.f1.|)|E) <= Integral(M,|.f1.|) by A5,RELAT_1:97; then
A13: Integral(M,(|.f1.|)|E) <= Integral(M,|.f.|) by MESFUNC6:1;
   |.g1.| is_integrable_on M by A1,A4,MESFUNC5:106; then
   ex E be Element of S st E = dom |.g1.| & |.g1.| is_measurable_on E
     by MESFUNC5:def 17; then
   Integral(M,(|.g1.|)|E) <= Integral(M,(|.g1.|)|C)
     by A5,A10,MESFUNC5:99; then
   Integral(M,(|.g1.|)|E) <= Integral(M,|.g1.|) by A5,RELAT_1:97; then
   Integral(M,(|.g1.|)|E) <= Integral(M,|.g.|) by MESFUNC6:1; then
   Integral(M,(|.f1.|)|E) + Integral(M,(|.g1.|)|E)
    <= Integral(M,|.f.|) + Integral(M,|.g.|) by A13,SUPINF_2:14;
   hence thesis by A2,A8,XXREAL_0:2;
end;

Th26: L-1-Space M is RealNormSpace-like RealLinearSpace-like Abelian
               add-associative right_zeroed right_complementable
proof
   now let x,y be Point of L-1-Space M, a be Real;
    hereby assume A2: ||.x.|| = 0;
     reconsider x1 =x as Point of Pre-L-Space M;
     consider f be PartFunc of X, REAL such that
A3:   f in x1 and (L-1-Norm M).x1 = Integral(M,abs f) by Def20;
A4:  Integral(M,abs f) = 0 by A2,A3,Lm17x;
     set g = X-->0;
A6:  f in L1_Functions M & f is_integrable_on M by Lm16,A3; then
A5:  f a.e.= g,M by A4,Lm261;
A8:  g in L1_Functions M by LmDef1;
A7:  a.e-eq-class(g,M) = a.e-eq-class(f,M) by A5,A6,A8,EQC02;
     a.e-eq-class(f,M) in CosetSet M by A6; then
     zeroCoset M = a.e-eq-class(f,M) by VSPDef4X,A7,A8; then
     0.(Pre-L-Space M) = a.e-eq-class(f,M) by VSPDef6X;
     hence x =0.(L-1-Space M) by A3,Lm17z;
    end;
    hereby assume A10: x = 0.(L-1-Space M);
     reconsider x1 =x as Point of Pre-L-Space M;
     x1 =0.(Pre-L-Space M) by A10; then
A11: x1 = zeroCoset M by VSPDef6X;
     consider f be PartFunc of X,REAL such that
A12:  f = X-->0 & f in L1_Functions M &
      zeroCoset M = a.e-eq-class(f,M) by VSPDef4X;
     (L-1-Norm M).x1 = ||.x.||; then
     (L-1-Norm M).x1 = Integral(M,abs f) by EQC01,A11,A12,Lm17x;
     hence ||.x.||=0 by A12,Lm262;
    end;
    consider f be PartFunc of X,REAL such that
A15: f in x & ||.x.|| = Integral(M,abs f) by Def20;
    consider g be PartFunc of X,REAL such that
A16: g in y & ||.y.|| = Integral(M,abs g) by Def20;
A17:f in L1_Functions M & f is_integrable_on M by Lm16,A15; then
    |. Integral(M,f) .| <= Integral(M,abs f) by MESFUNC6:95;
    hence 0 <= ||.x.|| by A15,EXTREAL2:51;
    f+g in x+y by Lm17Y,A15,A16; then
A20:||.x+y.|| = Integral(M,abs(f+g)) by Lm17x;
A21:Integral(M,abs f) + Integral(M,abs g) = ||.x.|| + ||.y.||
      by A15,A16,SUPINF_2:1;
    g in L1_Functions M & g is_integrable_on M by Lm16,A16;
    hence ||.x+y.|| <= ||.x.|| + ||.y.|| by Lm263,A20,A21,A17;
A25:a(#)f in a*x by Lm17Y,A15;
    abs f is_integrable_on M by Lm16,A15; then
    Integral(M,abs a(#)abs f) =R_EAL(abs a) * Integral(M,abs f)
       by MESFUNC6:102; then
    Integral(M,abs(a(#)f)) = R_EAL(abs a) * Integral(M,abs f)
       by RFUNCT_1:37; then
    Integral(M,abs(a(#)f)) = abs a * ||.x.|| by A15,EXTREAL1:13;
    hence ||.a*x.|| = abs a * ||.x.|| by A25,Lm17x;
   end;
   hence thesis by NORMSP_1:def 2,RSSPACE3:4;
end;

registration
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  cluster L-1-Space M -> RealNormSpace-like RealLinearSpace-like
               Abelian add-associative right_zeroed right_complementable;
  coherence by Th26;
end;