lpspace1.miz



    begin

    definition

      let V be non empty RLSStruct, V1 be Subset of V;

      :: LPSPACE1:def1

      attr V1 is multi-closed means

      : Def1: for a be Real, v be VECTOR of V st v in V1 holds (a * v) in V1;

    end

    theorem :: LPSPACE1:1

    for V be RealLinearSpace, V1 be Subset of V holds V1 is linearly-closed iff V1 is add-closed multi-closed by RLSUB_1:def 1;

    registration

      let V be non empty RLSStruct;

      cluster add-closed multi-closed non empty for Subset of V;

      existence

      proof

        set M = the carrier of V;

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

        thus thesis;

      end;

    end

    definition

      let X be non empty RLSStruct;

      let X1 be multi-closed non empty Subset of X;

      :: LPSPACE1:def2

      func Mult_ X1 -> Function of [: REAL , X1:], X1 equals (the Mult of X | [: REAL , X1:]);

      correctness

      proof

        

         A1: [: REAL , X1:] c= [: REAL , the carrier of X:] & ( dom the Mult of X) = [: REAL , the carrier of X:] by FUNCT_2:def 1, ZFMISC_1: 95;

         A2:

        now

          let z be object;

          assume

           A3: z in [: REAL , X1:];

          then

          consider r,x be object such that

           A4: r in REAL and

           A5: x in X1 and

           A6: z = [r, x] by ZFMISC_1:def 2;

          reconsider r as Real by A4;

          reconsider y = x as VECTOR of X by A5;

           [r, x] in ( dom (the Mult of X | [: REAL , X1:])) by A1, A3, A6, RELAT_1: 62;

          then ((the Mult of X | [: REAL , X1:]) . z) = (r * y) by A6, FUNCT_1: 47;

          hence ((the Mult of X | [: REAL , X1:]) . z) in X1 by A5, Def1;

        end;

        ( dom (the Mult of X | [: REAL , X1:])) = [: REAL , X1:] by A1, RELAT_1: 62;

        hence thesis by A2, FUNCT_2: 3;

      end;

    end

    reserve a,b,r for Real;

    theorem :: LPSPACE1:2

    

     Th2: for V be Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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 vector-distributive scalar-distributive scalar-associative scalar-unital

    proof

      let V be Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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

       A1: d1 = ( 0. V) and

       A2: A = (the addF of V || V1) and

       A3: M = (the Mult of V | [: REAL , V1:]);

      set W = RLSStruct (# D, d1, A, M #);

       A4:

      now

        let a;

        reconsider aa = a as Element of REAL by XREAL_0:def 1;

        let x be VECTOR of W;

        

        thus (a * x) = (the Mult of V . [aa, x]) by A3, FUNCT_1: 49

        .= (the Mult of V . (a,x));

      end;

       A5:

      now

        let x,y be VECTOR of W;

        

        thus (x + y) = (the addF of V . [x, y]) by A2, FUNCT_1: 49

        .= (the addF of V . (x,y));

      end;

      W is Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital

      proof

        set Mv = the Mult of V;

        set Av = the addF 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 A5

          .= (y1 + x1)

          .= (y + x) by A5;

        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 A5

          .= ((x1 + y1) + z1) by A5

          .= (x1 + (y1 + z1)) by RLVECT_1:def 3

          .= (Av . (x1,(y + z))) by A5

          .= (x + (y + z)) by A5;

        end;

        hence W is add-associative;

        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 A1, A5

          .= x by RLVECT_1:def 4;

        end;

        hence W is right_zeroed;

        hereby

          let a1 be Real;

          let x,y be VECTOR of W;

          reconsider a = a1 as Real;

          reconsider x1 = x, y1 = y as VECTOR of V by TARSKI:def 3;

          (a * (x + y)) = (Mv . (a,(x + y))) by A4

          .= (a * (x1 + y1)) by A5

          .= ((a * x1) + (a * y1)) by RLVECT_1:def 5

          .= (Av . ((Mv . (a,x1)),(a * y))) by A4

          .= (Av . ((a * x),(a * y))) by A4

          .= ((a * x) + (a * y)) by A5;

          hence (a1 * (x + y)) = ((a1 * x) + (a1 * y));

        end;

        hereby

          let a1,b1 be Real;

          let x be VECTOR of W;

          reconsider a = a1, b = b1 as Real;

          reconsider y = x as VECTOR of V by TARSKI:def 3;

          ((a + b) * x) = ((a + b) * y) by A4

          .= ((a * y) + (b * y)) by RLVECT_1:def 6

          .= (Av . ((Mv . (a,y)),(b * x))) by A4

          .= (Av . ((a * x),(b * x))) by A4

          .= ((a * x) + (b * x)) by A5;

          hence ((a1 + b1) * x) = ((a1 * x) + (b1 * x));

        end;

        hereby

          let a1,b1 be Real;

          let x be VECTOR of W;

          reconsider a = a1, b = b1 as Real;

          reconsider y = x as VECTOR of V by TARSKI:def 3;

          ((a * b) * x) = ((a * b) * y) by A4

          .= (a * (b * y)) by RLVECT_1:def 7

          .= (Mv . (a,(b * x))) by A4

          .= (a * (b * x)) by A4;

          hence ((a1 * b1) * x) = (a1 * (b1 * x));

        end;

        let x be VECTOR of W;

        reconsider y = x as VECTOR of V by TARSKI:def 3;

        

        thus (1 * x) = (1 * y) by A4

        .= x by RLVECT_1:def 8;

      end;

      hence thesis;

    end;

    theorem :: LPSPACE1:3

    

     Th3: for V be Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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 vector-distributive scalar-distributive scalar-associative scalar-unital

    proof

      let V be Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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) by SUBSET_1:def 8;

      hence thesis by Th2;

    end;

    theorem :: LPSPACE1:4

    

     Th4: 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) by ZFMISC_1: 87, FUNCT_1: 49;

    theorem :: LPSPACE1:5

    

     Th5: 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) #);

      reconsider a as Element of REAL by XREAL_0:def 1;

      assume

       A1: w = v;

      then [a, v] in [: REAL , V1:] by ZFMISC_1: 87;

      hence thesis by A1, FUNCT_1: 49;

    end;

    begin

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

      :: original: .

      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;

      :: LPSPACE1:def3

      func multpfunc A -> BinOp of ( PFuncs (A, REAL )) means

      : Def3: for f,g be 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 be 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

         A1: for f, g holds (it1 . (f,g)) = (f (#) g) and

         A2: for f, g holds (it2 . (f,g)) = (f (#) g);

        now

          let f, g;

          

          thus (it1 . (f,g)) = (f (#) g) by A1

          .= (it2 . (f,g)) by A2;

        end;

        hence thesis;

      end;

    end

    definition

      let A;

      :: LPSPACE1:def4

      func multrealpfunc A -> Function of [: REAL , ( PFuncs (A, REAL )):], ( PFuncs (A, REAL )) means

      : Def4: for a be Real, f be 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);

        consider F be Function of [: REAL , ( PFuncs (A, REAL )):], ( PFuncs (A, REAL )) such that

         A1: for a be Element of REAL , f holds (F . (a,f)) = F(a,f) from BINOP_1:sch 4;

        take F;

        let a be Real, f be Element of ( PFuncs (A, REAL ));

        reconsider a as Element of REAL by XREAL_0:def 1;

        (F . (a,f)) = F(a,f) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let it1,it2 be Function of [: REAL , ( PFuncs (A, REAL )):], ( PFuncs (A, REAL )) such that

         A2: for a be Real, f be Element of ( PFuncs (A, REAL )) holds (it1 . (a,f)) = (a (#) f) and

         A3: for a be Real, f be 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;

      end;

    end

    definition

      let A;

      :: LPSPACE1:def5

      func RealPFuncZero A -> Element of ( PFuncs (A, REAL )) equals (A --> 0 );

      coherence

      proof

        (A --> ( In ( 0 , REAL ))) is Function of A, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

    end

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    definition

      let A;

      :: LPSPACE1:def6

      func RealPFuncUnit A -> Element of ( PFuncs (A, REAL )) equals (A --> 1);

      coherence

      proof

        (A --> jj) is Function of A, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

    end

    theorem :: LPSPACE1:6

    

     Th6: h = (( addpfunc A) . (f,g)) iff (( dom h) = (( dom f) /\ ( dom g)) & for x be 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

         A2: x in ( dom (f + g)) by A1, RFUNCT_3:def 4;

        (h . x) = ((f + g) . x) by A1, RFUNCT_3:def 4;

        hence (h . x) = ((f . x) + (g . x)) by A2, VALUED_1:def 1;

      end;

      assume that

       A3: ( dom h) = (( dom f) /\ ( dom g)) and

       A4: for x be Element of A st x in ( dom h) holds (h . x) = ((f . x) + (g . x));

      set k = (( addpfunc A) . (f,g));

       A5:

      now

        let x be Element of A;

        

         A6: (k . x) = ((f + g) . x) by RFUNCT_3:def 4;

        assume

         A7: x in ( dom h);

        then x in ( dom (f + g)) by A3, VALUED_1:def 1;

        

        hence (k . x) = ((f . x) + (g . x)) by A6, VALUED_1:def 1

        .= (h . x) by A4, A7;

      end;

      ( dom k) = ( dom (f + g)) by RFUNCT_3:def 4

      .= ( dom h) by A3, VALUED_1:def 1;

      hence thesis by A5, PARTFUN1: 5;

    end;

    theorem :: LPSPACE1:7

    

     Th7: h = (( multpfunc A) . (f,g)) iff ( dom h) = (( dom f) /\ ( dom g)) & for x be Element of A st x in ( dom h) holds (h . x) = ((f . x) * (g . x))

    proof

      set k = (( multpfunc A) . (f,g));

      hereby

        assume

         A1: 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

         A2: x in ( dom (f (#) g)) by A1, Def3;

        (h . x) = ((f (#) g) . x) by A1, Def3;

        hence (h . x) = ((f . x) * (g . x)) by A2, VALUED_1:def 4;

      end;

      assume that

       A3: ( dom h) = (( dom f) /\ ( dom g)) and

       A4: for x be Element of A st x in ( dom h) holds (h . x) = ((f . x) * (g . x));

       A5:

      now

        let x be Element of A;

        

         A6: (k . x) = ((f (#) g) . x) by Def3;

        assume

         A7: x in ( dom h);

        then x in ( dom (f (#) g)) by A3, VALUED_1:def 4;

        

        hence (k . x) = ((f . x) * (g . x)) by A6, VALUED_1:def 4

        .= (h . x) by A4, A7;

      end;

      ( dom k) = ( dom (f (#) g)) by Def3

      .= ( dom h) by A3, VALUED_1:def 4;

      hence thesis by A5, PARTFUN1: 5;

    end;

    theorem :: LPSPACE1:8

    ( RealPFuncZero A) <> ( RealPFuncUnit A)

    proof

      set a = the Element of A;

      (( RealPFuncZero A) . a) = 0 by FUNCOP_1: 7;

      hence thesis by FUNCOP_1: 7;

    end;

    theorem :: LPSPACE1:9

    

     Th9: h = (( multrealpfunc A) . (a,f)) iff ( dom h) = ( dom f) & for x be Element of A st x in ( dom f) holds (h . x) = (a * (f . x))

    proof

      hereby

        assume

         A1: 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 A1, Def4;

      end;

      hereby

        reconsider aa = a as Element of REAL by XREAL_0:def 1;

        reconsider k = (( multrealpfunc A) . (aa,f)) as Element of ( PFuncs (A, REAL ));

        assume that

         A2: ( dom f) = ( dom h) and

         A3: for x be Element of A st x in ( dom f) holds (h . x) = (a * (f . x));

         A4:

        now

          let x be Element of A;

          assume

           A5: 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 A3, A5;

          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 A2, A4, PARTFUN1: 5;

      end;

    end;

    theorem :: LPSPACE1:10

    

     Th10: (( addpfunc A) . (f,g)) = (( addpfunc A) . (g,f)) by RFUNCT_3: 14, BINOP_1:def 2;

    theorem :: LPSPACE1:11

    

     Th11: (( addpfunc A) . (f,(( addpfunc A) . (g,h)))) = (( addpfunc A) . ((( addpfunc A) . (f,g)),h)) by RFUNCT_3: 15, BINOP_1:def 3;

    theorem :: LPSPACE1:12

    (( multpfunc A) . (f,g)) = (( multpfunc A) . (g,f))

    proof

      

       A1: ( dom (( multpfunc A) . (g,f))) = (( dom g) /\ ( dom f)) by Th7;

      

       A2: ( dom (( multpfunc A) . (f,g))) = (( dom f) /\ ( dom g)) by Th7;

      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 A2, Th7

        .= ((( multpfunc A) . (g,f)) . x) by A1, A3, Th7;

      end;

      hence thesis by A2, A1, PARTFUN1: 5;

    end;

    theorem :: LPSPACE1:13

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

      

       A1: ( dom k1) = (( dom k) /\ ( dom h)) by Th7;

      then

       A2: ( dom k1) c= ( dom k) by XBOOLE_1: 17;

      

       A3: ( dom k1) = ((( dom f) /\ ( dom g)) /\ ( dom h)) by A1, Th7;

      

       A4: ( dom j1) = (( dom f) /\ ( dom j)) by Th7;

      then

       A5: ( dom j1) = (( dom f) /\ (( dom g) /\ ( dom h))) by Th7;

      

       A6: ( dom j1) c= ( dom j) by A4, XBOOLE_1: 17;

      now

        let x be Element of A;

        assume

         A7: x in ( dom j1);

        then

         A8: x in ( dom k1) by A5, A3, XBOOLE_1: 16;

        

        thus (j1 . x) = ((f . x) * (j . x)) by A7, Th7

        .= ((f . x) * ((g . x) * (h . x))) by A6, A7, Th7

        .= (((f . x) * (g . x)) * (h . x))

        .= ((k . x) * (h . x)) by A2, A8, Th7

        .= (k1 . x) by A8, Th7;

      end;

      hence thesis by A5, A3, PARTFUN1: 5, XBOOLE_1: 16;

    end;

    theorem :: LPSPACE1:14

    (( multpfunc A) . (( RealPFuncUnit A),f)) = f

    proof

      set h = (( multpfunc A) . (( RealPFuncUnit A),f));

      ( dom h) = (( dom ( RealPFuncUnit A)) /\ ( dom f)) by Th7;

      then ( dom h) = (A /\ ( dom f)) by FUNCOP_1: 13;

      then

       A1: ( 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 A1, Th7;

        then (h . x) = (1 * (f . x)) by FUNCOP_1: 7;

        hence (h . x) = (f . x);

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: LPSPACE1:15

    

     Th15: (( addpfunc A) . (( RealPFuncZero A),f)) = f

    proof

      set h = (( addpfunc A) . (( RealPFuncZero A),f));

      ( dom h) = (( dom ( RealPFuncZero A)) /\ ( dom f)) by Th6;

      then ( dom h) = (A /\ ( dom f)) by FUNCOP_1: 13;

      then

       A1: ( dom h) = ( dom f) by XBOOLE_1: 28;

      now

        let x be Element of A;

        

         A2: (( RealPFuncZero A) . x) = 0 by FUNCOP_1: 7;

        assume x in ( dom f);

        

        hence (h . x) = ( 0 + (f . x)) by A1, A2, Th6

        .= (f . x);

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: LPSPACE1:16

    

     Th16: (( addpfunc A) . (f,(( multrealpfunc A) . (( - 1),f)))) = (( RealPFuncZero A) | ( dom f))

    proof

      reconsider g = (( multrealpfunc A) . (( - jj),f)) as Element of ( PFuncs (A, REAL ));

      set h = (( addpfunc A) . (f,g));

      ( dom ( RealPFuncZero A)) = A by FUNCOP_1: 13;

      then ( dom (( RealPFuncZero A) | ( dom f))) = (A /\ ( dom f)) by RELAT_1: 61;

      then

       A1: ( dom (( RealPFuncZero A) | ( dom f))) = ( dom f) by XBOOLE_1: 28;

      

       A2: ( dom h) = (( dom g) /\ ( dom f)) by Th6

      .= (( dom f) /\ ( dom f)) by Th9;

      now

        let x be Element of A;

        assume

         A3: x in ( dom f);

        then

         A4: x in ( dom (( - 1) (#) f)) by VALUED_1:def 5;

        

        thus (h . x) = ((f . x) + (g . x)) by A2, A3, Th6

        .= ((f . x) + ((( - 1) (#) f) . x)) by Def4

        .= ((f . x) + (( - 1) * (f . x))) by A4, VALUED_1:def 5

        .= (( RealPFuncZero A) . x) by FUNCOP_1: 7

        .= ((( RealPFuncZero A) | ( dom f)) . x) by A3, FUNCT_1: 49;

      end;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: LPSPACE1:17

    

     Th17: (( multrealpfunc A) . (1,f)) = f

    proof

      reconsider g = (( multrealpfunc A) . (jj,f)) as Element of ( PFuncs (A, REAL ));

       A1:

      now

        let x be Element of A;

        assume x in ( dom f);

        

        hence (g . x) = (1 * (f . x)) by Th9

        .= (f . x);

      end;

      ( dom g) = ( dom f) by Th9;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: LPSPACE1:18

    

     Th18: (( multrealpfunc A) . (a,(( multrealpfunc A) . (b,f)))) = (( multrealpfunc A) . ((a * b),f))

    proof

      reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;

      reconsider g = (( multrealpfunc A) . (bb,f)) as Element of ( PFuncs (A, REAL ));

      reconsider h = (( multrealpfunc A) . (aa,g)) as Element of ( PFuncs (A, REAL ));

      reconsider k = (( multrealpfunc A) . ((aa * bb),f)) as Element of ( PFuncs (A, REAL ));

      

       A1: ( dom h) = ( dom g) by Th9;

      

       A2: ( dom g) = ( dom f) by Th9;

       A3:

      now

        let x be Element of A;

        assume

         A4: x in ( dom h);

        

        hence (h . x) = (a * (g . x)) by A1, Th9

        .= (a * (b * (f . x))) by A2, A1, A4, Th9

        .= ((a * b) * (f . x))

        .= (k . x) by A2, A1, A4, Th9;

      end;

      ( dom k) = ( dom f) by Th9;

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

    end;

    theorem :: LPSPACE1:19

    

     Th19: (( addpfunc A) . ((( multrealpfunc A) . (a,f)),(( multrealpfunc A) . (b,f)))) = (( multrealpfunc A) . ((a + b),f))

    proof

      reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;

      reconsider g = (( multrealpfunc A) . (aa,f)) as Element of ( PFuncs (A, REAL ));

      reconsider h = (( multrealpfunc A) . (bb,f)) as Element of ( PFuncs (A, REAL ));

      reconsider k = (( multrealpfunc A) . ((aa + bb),f)) as Element of ( PFuncs (A, REAL ));

      set j = (( addpfunc A) . (g,h));

      ( dom g) = ( dom f) by Th9;

      then (( dom h) /\ ( dom g)) = (( dom f) /\ ( dom f)) by Th9;

      then

       A1: ( dom j) = ( dom f) by Th6;

       A2:

      now

        let x be Element of A;

        assume

         A3: x in ( dom j);

        then x in ( dom (b (#) f)) by A1, VALUED_1:def 5;

        then ((b (#) f) . x) = (b * (f . x)) by VALUED_1:def 5;

        then

         A4: (h . x) = (b * (f . x)) by Def4;

        x in ( dom (a (#) f)) by A1, A3, VALUED_1:def 5;

        then ((a (#) f) . x) = (a * (f . x)) by VALUED_1:def 5;

        then (g . x) = (a * (f . x)) by Def4;

        then ((g . x) + (h . x)) = ((a + b) * (f . x)) by A4;

        

        hence (j . x) = ((a + b) * (f . x)) by A3, Th6

        .= (k . x) by A1, A3, Th9;

      end;

      ( dom k) = ( dom f) by Th9;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    

     Lm1: (( addpfunc A) . ((( multrealpfunc A) . (a,f)),(( multrealpfunc A) . (a,g)))) = (( multrealpfunc A) . (a,(( addpfunc A) . (f,g))))

    proof

      reconsider aa = a as Element of REAL by XREAL_0:def 1;

      reconsider h = (( multrealpfunc A) . (aa,f)) as Element of ( PFuncs (A, REAL ));

      reconsider i = (( multrealpfunc A) . (aa,g)) as Element of ( PFuncs (A, REAL ));

      set j = (( addpfunc A) . (f,g));

      reconsider k = (( multrealpfunc A) . (aa,j)) as Element of ( PFuncs (A, REAL ));

      set l = (( addpfunc A) . (h,i));

      

       A1: ( dom h) = ( dom f) & ( dom i) = ( dom g) by Th9;

      

       A2: ( dom l) = (( dom h) /\ ( dom i)) by Th6;

      

       A3: ( dom j) = (( dom f) /\ ( dom g)) by Th6;

       A4:

      now

        let x be Element of A;

        

         A5: (h . x) = ((a (#) f) . x) by Def4;

        assume

         A6: x in ( dom l);

        then

         A7: x in ( dom (f + g)) by A1, A2, VALUED_1:def 1;

        

         A8: (i . x) = ((a (#) g) . x) by Def4;

        x in ( dom i) by A2, A6, XBOOLE_0:def 4;

        then x in ( dom g) by Th9;

        then x in ( dom (a (#) g)) by VALUED_1:def 5;

        then

         A9: (i . x) = (a * (g . x)) by A8, VALUED_1:def 5;

        x in ( dom h) by A2, A6, XBOOLE_0:def 4;

        then x in ( dom f) by Th9;

        then x in ( dom (a (#) f)) by VALUED_1:def 5;

        then

         A10: (h . x) = (a * (f . x)) by A5, VALUED_1:def 5;

        

        thus (l . x) = ((h . x) + (i . x)) by A6, Th6

        .= (a * ((f . x) + (g . x))) by A10, A9

        .= (a * ((f + g) . x)) by A7, VALUED_1:def 1

        .= (a * (j . x)) by RFUNCT_3:def 4

        .= (k . x) by A1, A3, A2, A6, Th9;

      end;

      ( dom k) = ( dom j) by Th9;

      hence thesis by A1, A3, A2, A4, PARTFUN1: 5;

    end;

    theorem :: LPSPACE1:20

    (( 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 f) /\ ( dom g)) /\ ( dom h)) = (( dom f) /\ (( dom g) /\ ( dom h))) by XBOOLE_1: 16;

      ( dom i) = (( dom f) /\ ( dom h)) & ( dom j) = (( dom f) /\ ( dom g)) by Th7;

      then ( dom k) = ((( dom h) /\ ( dom f)) /\ (( dom f) /\ ( dom g))) by Th6;

      then ( dom k) = (( dom h) /\ (( dom f) /\ (( dom f) /\ ( dom g)))) by XBOOLE_1: 16;

      then

       A2: ( dom k) = (( dom h) /\ ((( dom f) /\ ( dom f)) /\ ( dom g))) by XBOOLE_1: 16;

      

       A3: ((( dom f) /\ ( dom g)) /\ ( dom h)) = (( dom g) /\ (( dom f) /\ ( dom h))) by XBOOLE_1: 16;

       A4:

      now

        let x be Element of A;

        assume

         A5: x in ( dom k);

        then x in (( dom f) /\ ( dom g)) by A2, XBOOLE_0:def 4;

        then

         A6: x in ( dom (f (#) g)) by VALUED_1:def 4;

        x in (( dom g) /\ ( dom h)) by A2, A1, A5, XBOOLE_0:def 4;

        then

         A7: x in ( dom (g + h)) by VALUED_1:def 1;

        (j . x) = ((f (#) g) . x) by Def3;

        then

         A8: (j . x) = ((f . x) * (g . x)) by A6, VALUED_1:def 4;

        x in (( dom f) /\ ( dom h)) by A2, A3, A5, XBOOLE_0:def 4;

        then

         A9: x in ( dom (f (#) h)) by VALUED_1:def 4;

        (i . x) = ((f (#) h) . x) by Def3;

        then

         A10: (i . x) = ((f . x) * (h . x)) by A9, VALUED_1:def 4;

        (k . x) = ((j . x) + (i . x)) by A5, Th6;

        then (l . x) = ((g + h) . x) & (k . x) = ((f . x) * ((g . x) + (h . x))) by A8, A10, RFUNCT_3:def 4;

        then

         A11: (k . x) = ((f . x) * (l . x)) by A7, VALUED_1:def 1;

        x in (( dom f) /\ ( dom l)) by A2, A1, A5, Th6;

        then

         A12: x in ( dom (f (#) l)) by VALUED_1:def 4;

        (m . x) = ((f (#) l) . x) by Def3;

        hence (k . x) = (m . x) by A12, A11, VALUED_1:def 4;

      end;

      ( dom m) = (( dom f) /\ ( dom l)) & ( dom l) = (( dom g) /\ ( dom h)) by Th6, Th7;

      hence thesis by A2, A4, PARTFUN1: 5, XBOOLE_1: 16;

    end;

    theorem :: LPSPACE1:21

    (( multpfunc A) . ((( multrealpfunc A) . (a,f)),g)) = (( multrealpfunc A) . (a,(( multpfunc A) . (f,g))))

    proof

      reconsider aa = a as Element of REAL by XREAL_0:def 1;

      reconsider i = (( multrealpfunc A) . (aa,f)) as Element of ( PFuncs (A, REAL ));

      set j = (( multpfunc A) . (f,g));

      set k = (( multpfunc A) . (i,g));

      reconsider l = (( multrealpfunc A) . (aa,j)) as Element of ( PFuncs (A, REAL ));

      

       A1: ( dom i) = ( dom f) & ( dom k) = (( dom i) /\ ( dom g)) by Th7, Th9;

      

       A2: ( dom j) = (( dom f) /\ ( dom g)) by Th7;

       A3:

      now

        let x be Element of A;

        

         A4: (j . x) = ((f (#) g) . x) by Def3;

        assume

         A5: x in ( dom k);

        then x in ( dom (f (#) g)) by A1, VALUED_1:def 4;

        then

         A6: (j . x) = ((f . x) * (g . x)) by A4, VALUED_1:def 4;

        

         A7: (i . x) = ((a (#) f) . x) & ( dom (a (#) f)) = ( dom f) by Def4, VALUED_1:def 5;

        x in ( dom f) by A1, A5, XBOOLE_0:def 4;

        then

         A8: (i . x) = (a * (f . x)) by A7, VALUED_1:def 5;

        

         A9: (l . x) = ((a (#) j) . x) by Def4;

        x in ( dom (a (#) j)) by A1, A2, A5, VALUED_1:def 5;

        then

         A10: (l . x) = (a * ((f . x) * (g . x))) by A6, A9, VALUED_1:def 5;

        (k . x) = ((i . x) * (g . x)) by A5, Th7;

        hence (k . x) = (l . x) by A8, A10;

      end;

      ( dom l) = ( dom j) by Th9;

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

    end;

    definition

      let A;

      :: LPSPACE1:def7

      func RLSp_PFunct A -> non empty RLSStruct equals RLSStruct (# ( PFuncs (A, REAL )), ( RealPFuncZero A), ( addpfunc A), ( multrealpfunc A) #);

      coherence ;

    end

    reserve u,v,w for VECTOR of ( RLSp_PFunct A);

    registration

      let A;

      cluster ( RLSp_PFunct A) -> strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        set IT = ( RLSp_PFunct A);

        thus IT is strict;

        thus (u + v) = (v + u) by Th10;

        thus ((u + v) + w) = (u + (v + w)) by Th11;

        thus (u + ( 0. IT)) = u

        proof

          reconsider u9 = u as Element of ( PFuncs (A, REAL ));

          

          thus (u + ( 0. IT)) = (( addpfunc A) . (( RealPFuncZero A),u9)) by Th10

          .= u by Th15;

        end;

        thus for a be Real, u, v holds (a * (u + v)) = ((a * u) + (a * v)) by Lm1;

        thus for a,b be Real, v holds ((a + b) * v) = ((a * v) + (b * v)) by Th19;

        thus for a,b be Real, v holds ((a * b) * v) = (a * (b * v)) by Th18;

        let v;

        thus (1 * v) = v by Th17;

      end;

    end

    begin

    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 for Element of S,

f,g,h,f1,g1 for PartFunc of X, REAL ;

    theorem :: LPSPACE1:22

    

     Th22: for X, S, M holds 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 ;

      given E such that

       A1: E = ( dom f);

      assume

       A2: for x st x in ( dom f) holds 0 = (f . x);

      then

       A3: for x be object st x in ( dom f) holds (f . x) = 0 ;

      then

       A4: f is_simple_func_in S by A1, MESFUNC6: 2;

      then

       A5: ( integral+ (M,f)) = 0 by A1, A2, MESFUNC2: 34, MESFUNC5: 87;

      

       A6: ( dom ( max+ f)) = ( dom f) by MESFUNC2:def 2;

       A7:

      now

        let x be Element of X;

        assume

         A8: x in ( dom f);

        

        hence (f . x) = ( max ( 0 , 0 )) by A2

        .= ( max ((f . x), 0 )) by A2, A8

        .= (( max+ f) . x) by A6, A8, MESFUNC2:def 2;

      end;

      

       A9: f is E -measurable by A1, A3, MESFUNC2: 34, MESFUNC6: 2;

      

       A10: f is nonnegative

      proof

        let y be ExtReal;

        assume y in ( rng f);

        then ex x1 be object st x1 in ( dom f) & y = (f . x1) by FUNCT_1:def 3;

        hence y >= 0 by A2;

      end;

      

      then 0. = ( Integral (M,f)) by A1, A4, A5, MESFUNC2: 34, MESFUNC5: 88

      .= (( integral+ (M,f)) - ( integral+ (M,( max- f)))) by A6, A7, PARTFUN1: 5

      .= ( 0. + ( - ( integral+ (M,( max- f))))) by A1, A2, A4, MESFUNC2: 34, MESFUNC5: 87

      .= ( - ( integral+ (M,( max- f)))) by XXREAL_3: 4;

      then

       A11: ( - ( - ( integral+ (M,( max- f))))) = ( - 0 );

      ( integral+ (M,( max+ f))) < +infty by A6, A7, A5, PARTFUN1: 5;

      hence f is_integrable_on M by A1, A9, A11;

      thus thesis by A1, A9, A5, A10, MESFUNC5: 88;

    end;

    definition

      let X be non empty set, r be Real;

      :: original: -->

      redefine

      func X --> r -> PartFunc of X, REAL ;

      coherence

      proof

        reconsider r as Element of REAL by XREAL_0:def 1;

        (X --> r) is PartFunc of X, REAL ;

        hence thesis;

      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

      

       A1: X is Element of S by MEASURE1: 7;

      assume

       A2: X = ( dom f) & for x st x in ( dom f) holds 0 = (f . x);

      then ( R_EAL f) is_integrable_on M by A1, Th22;

      hence thesis by A2, Th22;

    end;

    definition

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

      :: LPSPACE1:def8

      func L1_Functions M -> non empty Subset of ( RLSp_PFunct X) equals { f where f be PartFunc of X, REAL : ex ND be Element of S st (M . ND) = 0 & ( dom f) = (ND ` ) & f is_integrable_on M };

      correctness

      proof

        reconsider ND = {} as Element of S by MEASURE1: 34;

        set g = (X --> 0 );

        set I = { f where f be 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 object;

          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 thesis by PARTFUN1: 45;

        end;

        

         A2: ( dom g) = (ND ` ) by FUNCOP_1: 13;

        for x be Element of X st x in ( dom g) holds (g . x) = 0 by FUNCOP_1: 7;

        then (M . ND) = 0 & g is_integrable_on M by A2, Lm2, VALUED_0:def 19;

        then g in I by A2;

        hence thesis by A1;

      end;

    end

    

     Lm3: (X --> 0 ) is PartFunc of X, REAL & (X --> 0 ) in ( L1_Functions M)

    proof

      reconsider g = (X --> ( In ( 0 , REAL ))) as Function of X, REAL by FUNCOP_1: 46;

      reconsider ND = {} as Element of S by MEASURE1: 34;

      

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

      then (M . ND) = 0 & g is_integrable_on M by A1, Lm2, VALUED_0:def 19;

      hence thesis by A1;

    end;

    

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

      then (E1 \/ E2) is measure_zero of M by MEASURE1: 37;

      hence thesis by MEASURE1:def 7;

    end;

    theorem :: LPSPACE1:23

    

     Th23: f in ( L1_Functions M) & g in ( L1_Functions M) implies (f + g) in ( L1_Functions M)

    proof

      set W = ( L1_Functions M);

      assume that

       A1: f in W and

       A2: g in W;

      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 by A1;

      then

      consider NDv be Element of S such that

       A3: (M . NDv) = 0 and

       A4: ( dom f) = (NDv ` ) and

       A5: 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 A2;

      then

      consider NDu be Element of S such that

       A6: (M . NDu) = 0 and

       A7: ( dom g) = (NDu ` ) and

       A8: g is_integrable_on M;

      

       A9: ( dom (f + g)) = ((NDv ` ) /\ (NDu ` )) by A4, A7, VALUED_1:def 1

      .= ((NDv \/ NDu) ` ) by XBOOLE_1: 53;

      (M . (NDv \/ NDu)) = 0 & (f + g) is_integrable_on M by A3, A5, A6, A8, Lm4, MESFUNC6: 100;

      hence thesis by A9;

    end;

    theorem :: LPSPACE1:24

    

     Th24: 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

       A1: (M . ND) = 0 and

       A2: ( dom f) = (ND ` ) & f is_integrable_on M;

      ( dom (a (#) f)) = (ND ` ) & (a (#) f) is_integrable_on M by A2, MESFUNC6: 102, VALUED_1:def 5;

      hence thesis by A1;

    end;

    

     Lm5: ( 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 ( RLSp_PFunct X) such that

         A1: v in W and

         A2: u in W;

        reconsider h = (v + u) as Element of ( PFuncs (X, REAL ));

        consider v1 be PartFunc of X, REAL such that

         A3: v1 = v and ex ND be Element of S st (M . ND) = 0 & ( dom v1) = (ND ` ) & v1 is_integrable_on M by A1;

        consider u1 be PartFunc of X, REAL such that

         A4: u1 = u and ex ND be Element of S st (M . ND) = 0 & ( dom u1) = (ND ` ) & u1 is_integrable_on M by A2;

        ( dom h) = (( dom v1) /\ ( dom u1)) & for x be object st x in ( dom h) holds (h . x) = ((v1 . x) + (u1 . x)) by A3, A4, Th6;

        then (v + u) = (v1 + u1) by VALUED_1:def 1;

        hence (v + u) in ( L1_Functions M) by A1, A2, A3, A4, Th23;

      end;

      hence ( L1_Functions M) is add-closed;

      now

        let a be Real, u be VECTOR of ( RLSp_PFunct X) such that

         A5: u in W;

        consider u1 be PartFunc of X, REAL such that

         A6: u1 = u and ex ND be Element of S st (M . ND) = 0 & ( dom u1) = (ND ` ) & u1 is_integrable_on M by A5;

        reconsider h = (a * u) as Element of ( PFuncs (X, REAL ));

        

         A7: ( dom h) = ( dom u1) by A6, Th9;

        then for x be object st x in ( dom h) holds (h . x) = (a * (u1 . x)) by A6, Th9;

        then (a * u) = (a (#) u1) by A7, VALUED_1:def 5;

        hence (a * u) in ( L1_Functions M) by A5, A6, Th24;

      end;

      hence thesis;

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

    end

    definition

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

      :: LPSPACE1:def9

      func RLSp_L1Funct M -> non empty RLSStruct equals RLSStruct (# ( L1_Functions M), ( In (( 0. ( RLSp_PFunct X)),( L1_Functions M))), ( add| (( L1_Functions M),( RLSp_PFunct X))), ( 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 vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        ( 0. ( RLSp_PFunct X)) in ( L1_Functions M) by Lm3;

        hence thesis by Th3;

      end;

    end

    begin

    reserve v,u for VECTOR of ( RLSp_L1Funct M);

    theorem :: LPSPACE1:25

    

     Th25: f = v & g = u implies (f + g) = (v + u)

    proof

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

      

       A1: ( dom h) = (( dom v3) /\ ( dom u3)) by Th6;

      assume

       A2: f = v & g = u;

      then for x be object st x in ( dom h) holds (h . x) = ((f . x) + (g . x)) by Th6;

      then h = (f + g) by A2, A1, VALUED_1:def 1;

      hence thesis by Th4;

    end;

    theorem :: LPSPACE1:26

    

     Th26: f = u implies (a (#) f) = (a * u)

    proof

      reconsider u2 = u as VECTOR of ( RLSp_PFunct X) by TARSKI:def 3;

      reconsider h = (a * u2) as Element of ( PFuncs (X, REAL ));

      assume

       A1: f = u;

      then

       A2: ( dom h) = ( dom f) by Th9;

      then for x be object st x in ( dom h) holds (h . x) = (a * (f . x)) by A1, Th9;

      then h = (a (#) f) by A2, VALUED_1:def 5;

      hence thesis by Th5;

    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 ;

      :: LPSPACE1:def10

      pred f a.e.= g,M means ex E be Element of S st (M . E) = 0 & (f | (E ` )) = (g | (E ` ));

    end

    theorem :: LPSPACE1:27

    

     Th27: 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_PFunct X) by TARSKI:def 3;

      reconsider h = (u2 + (( - 1) * u2)) as Element of ( PFuncs (X, REAL ));

      set g = (X --> 0 );

      (u + (( - 1) * u)) in ( L1_Functions M);

      then

      consider v be PartFunc of X, REAL such that

       A1: v = (u + (( - 1) * u)) and ex ND be Element of S st (M . ND) = 0 & ( dom v) = (ND ` ) & v is_integrable_on M;

      assume

       A2: f = u;

      then

       A3: h = (( RealPFuncZero X) | ( dom f)) by Th16;

      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

       A4: (M . ND) = 0 and

       A5: ( dom f) = (ND ` ) and f is_integrable_on M by A2;

      

       A6: (( - 1) * u2) = (( - 1) * u) by Th5;

      hence (u + (( - 1) * u)) = ((X --> 0 ) | ( dom f)) by A3, Th4;

      (v | (ND ` )) = ((g | (ND ` )) | (ND ` )) by A3, A6, A1, A5, Th4;

      then (v | (ND ` )) = (g | (ND ` )) by FUNCT_1: 51;

      then

       A7: v a.e.= (g,M) by A4;

      g in ( L1_Functions M) by Lm3;

      hence thesis by A1, A7;

    end;

    theorem :: LPSPACE1:28

    

     Th28: f a.e.= (f,M)

    proof

       {} is Element of S by PROB_1: 4;

      then

      consider E be Element of S such that

       A1: E = {} ;

      

       A2: (f | (E ` )) = (f | (E ` ));

      (M . E) = 0 by A1, VALUED_0:def 19;

      hence thesis by A2;

    end;

    theorem :: LPSPACE1:29

    f a.e.= (g,M) implies g a.e.= (f,M);

    theorem :: LPSPACE1:30

    

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

       A3: (M . EQ1) = 0 and

       A4: (f | (EQ1 ` )) = (g | (EQ1 ` )) by A1;

      consider EQ2 be Element of S such that

       A5: (M . EQ2) = 0 and

       A6: (g | (EQ2 ` )) = (h | (EQ2 ` )) by A2;

      

       A7: (M . (EQ1 \/ EQ2)) = 0 by A3, A5, Lm4;

      

       A8: ((EQ1 \/ EQ2) ` ) c= (EQ2 ` ) by XBOOLE_1: 7, XBOOLE_1: 34;

      

       A9: ((EQ1 \/ EQ2) ` ) c= (EQ1 ` ) by XBOOLE_1: 7, XBOOLE_1: 34;

      

      then (f | ((EQ1 \/ EQ2) ` )) = ((g | (EQ1 ` )) | ((EQ1 \/ EQ2) ` )) by A4, FUNCT_1: 51

      .= (g | ((EQ1 \/ EQ2) ` )) by A9, FUNCT_1: 51

      .= ((h | (EQ2 ` )) | ((EQ1 \/ EQ2) ` )) by A6, A8, FUNCT_1: 51

      .= (h | ((EQ1 \/ EQ2) ` )) by A8, FUNCT_1: 51;

      hence thesis by A7;

    end;

    theorem :: LPSPACE1:31

    

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

       A3: (M . EQ1) = 0 and

       A4: (f | (EQ1 ` )) = (f1 | (EQ1 ` )) by A1;

      consider EQ2 be Element of S such that

       A5: (M . EQ2) = 0 and

       A6: (g | (EQ2 ` )) = (g1 | (EQ2 ` )) by A2;

      

       A7: ((EQ1 \/ EQ2) ` ) c= (EQ1 ` ) by XBOOLE_1: 7, XBOOLE_1: 34;

      then (f | ((EQ1 \/ EQ2) ` )) = ((f1 | (EQ1 ` )) | ((EQ1 \/ EQ2) ` )) by A4, FUNCT_1: 51;

      then

       A8: (f | ((EQ1 \/ EQ2) ` )) = (f1 | ((EQ1 \/ EQ2) ` )) by A7, FUNCT_1: 51;

      

       A9: ((EQ1 \/ EQ2) ` ) c= (EQ2 ` ) by XBOOLE_1: 7, XBOOLE_1: 34;

      

      then (g | ((EQ1 \/ EQ2) ` )) = ((g1 | (EQ2 ` )) | ((EQ1 \/ EQ2) ` )) by A6, FUNCT_1: 51

      .= (g1 | ((EQ1 \/ EQ2) ` )) by A9, FUNCT_1: 51;

      

      then

       A10: ((f + g) | ((EQ1 \/ EQ2) ` )) = ((f1 | ((EQ1 \/ EQ2) ` )) + (g1 | ((EQ1 \/ EQ2) ` ))) by A8, RFUNCT_1: 44

      .= ((f1 + g1) | ((EQ1 \/ EQ2) ` )) by RFUNCT_1: 44;

      (M . (EQ1 \/ EQ2)) = 0 by A3, A5, Lm4;

      hence thesis by A10;

    end;

    theorem :: LPSPACE1:32

    

     Th32: f a.e.= (g,M) implies (a (#) f) a.e.= ((a (#) g),M)

    proof

      assume f a.e.= (g,M);

      then

      consider E be Element of S such that

       A1: (M . E) = 0 and

       A2: (f | (E ` )) = (g | (E ` ));

      ((a (#) f) | (E ` )) = (a (#) (g | (E ` ))) by A2, RFUNCT_1: 49

      .= ((a (#) g) | (E ` )) by RFUNCT_1: 49;

      hence thesis by A1;

    end;

    definition

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

      :: LPSPACE1:def11

      func AlmostZeroFunctions M -> non empty Subset of ( RLSp_L1Funct M) equals { f where f be PartFunc of X, REAL : f in ( L1_Functions M) & f a.e.= ((X --> 0 ),M) };

      coherence

      proof

         A1:

        now

          let x be object;

          assume x in { f where f be 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;

        (X --> 0 ) a.e.= ((X --> 0 ),M) & (X --> 0 ) in ( L1_Functions M) by Lm3, Th28;

        then (X --> 0 ) in { f where f be PartFunc of X, REAL : f in ( L1_Functions M) & f a.e.= ((X --> 0 ),M) };

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: LPSPACE1:33

    

     Th33: ((X --> 0 ) + (X --> 0 )) = (X --> 0 ) & (a (#) (X --> 0 )) = (X --> 0 )

    proof

      set g1 = (X --> 0 );

      set g2 = (X --> 0 );

       A1:

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

        hence ((a (#) g1) . x) = ((X --> 0 ) . x) by FUNCOP_1: 7;

      end;

      

       A2: ( 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 A2, VALUED_1:def 1;

        then ((g1 + g2) . x) = ( 0 + (g2 . x)) by FUNCOP_1: 7;

        hence ((g1 + g2) . x) = ((X --> 0 ) . x);

      end;

      hence (g1 + g2) = (X --> 0 ) by A2, PARTFUN1: 5;

      ( dom (a (#) g1)) = ( dom (X --> 0 )) by VALUED_1:def 5;

      hence thesis by A1, PARTFUN1: 5;

    end;

    

     Lm6: ( 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

         A1: v in Z and

         A2: u in Z;

        consider v1 be PartFunc of X, REAL such that

         A3: v1 = v and v1 in ( L1_Functions M) and

         A4: v1 a.e.= ((X --> 0 ),M) by A1;

        consider u1 be PartFunc of X, REAL such that

         A5: u1 = u and u1 in ( L1_Functions M) and

         A6: u1 a.e.= ((X --> 0 ),M) by A2;

        

         A7: (v + u) = (v1 + u1) by A3, A5, Th25;

        ((X --> 0 ) + (X --> 0 )) = (X --> 0 ) by Th33;

        then (v1 + u1) a.e.= ((X --> 0 ),M) by A4, A6, Th31;

        hence (v + u) in Z by A7;

      end;

      hence Z is add-closed;

      now

        let a be Real, u be VECTOR of V;

        assume u in Z;

        then

        consider u1 be PartFunc of X, REAL such that

         A8: u1 = u and u1 in ( L1_Functions M) and

         A9: u1 a.e.= ((X --> 0 ),M);

        

         A10: (a * u) = (a (#) u1) by A8, Th26;

        (a (#) (X --> 0 )) = (X --> 0 ) by Th33;

        then (a (#) u1) a.e.= ((X --> 0 ),M) by A9, Th32;

        hence (a * u) in Z by A10;

      end;

      hence thesis;

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

    end

    theorem :: LPSPACE1:34

    ( 0. ( RLSp_L1Funct M)) = (X --> 0 ) & ( 0. ( RLSp_L1Funct M)) in ( AlmostZeroFunctions M)

    proof

      thus ( 0. ( RLSp_L1Funct M)) = (X --> 0 ) by Lm3, SUBSET_1:def 8;

      (X --> 0 ) a.e.= ((X --> 0 ),M) & ( 0. ( RLSp_L1Funct M)) = ( 0. ( RLSp_PFunct X)) by Lm3, Th28, SUBSET_1:def 8;

      hence thesis;

    end;

    definition

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

      :: LPSPACE1:def12

      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 vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence ;

    end

    reserve v,u for VECTOR of ( RLSp_AlmostZeroFunct M);

    theorem :: LPSPACE1:35

    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 Th4

      .= (f + g) by A1, Th25;

    end;

    theorem :: LPSPACE1:36

    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 Th5

      .= (a (#) f) by A1, Th26;

    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 ;

      :: LPSPACE1:def13

      func a.e-eq-class (f,M) -> Subset of ( L1_Functions M) equals { g where g be 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 object;

          assume x in { g where g be 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 :: LPSPACE1:37

    

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

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

      end;

    end;

    theorem :: LPSPACE1:38

    

     Th38: 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 Th28;

        hence f in ( a.e-eq-class (f,M)) by A1;

      end;

    end;

    theorem :: LPSPACE1:39

    

     Th39: 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 that

       A1: f in ( L1_Functions M) and

       A2: 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 be PartFunc of X, REAL : r in ( L1_Functions M) & g in ( L1_Functions M) & g a.e.= (r,M) } by A1, Th38;

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

      end;

      assume

       A3: f a.e.= (g,M);

      now

        let x be object;

        assume x in ( a.e-eq-class (f,M));

        then

        consider r be PartFunc of X, REAL such that

         A4: x = r & r in ( L1_Functions M) and f in ( L1_Functions M) and

         A5: f a.e.= (r,M);

        g a.e.= (f,M) by A3;

        then g a.e.= (r,M) by A5, Th30;

        hence x in ( a.e-eq-class (g,M)) by A2, A4;

      end;

      then

       A6: ( a.e-eq-class (f,M)) c= ( a.e-eq-class (g,M));

      now

        let x be object;

        assume x in ( a.e-eq-class (g,M));

        then

        consider r be PartFunc of X, REAL such that

         A7: x = r & r in ( L1_Functions M) and g in ( L1_Functions M) and

         A8: g a.e.= (r,M);

        f a.e.= (r,M) by A3, A8, Th30;

        hence x in ( a.e-eq-class (f,M)) by A1, A7;

      end;

      then ( a.e-eq-class (g,M)) c= ( a.e-eq-class (f,M));

      hence thesis by A6, XBOOLE_0:def 10;

    end;

    theorem :: LPSPACE1:40

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

      hence thesis by A1, Th39;

    end;

    theorem :: LPSPACE1:41

    

     Th41: 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 that

       A1: f in ( L1_Functions M) & f1 in ( L1_Functions M) & g in ( L1_Functions M) & g1 in ( L1_Functions M) and

       A2: ( a.e-eq-class (f,M)) = ( a.e-eq-class (f1,M)) & ( a.e-eq-class (g,M)) = ( a.e-eq-class (g1,M));

      f a.e.= (f1,M) & g a.e.= (g1,M) by A1, A2, Th39;

      then

       A3: (f + g) a.e.= ((f1 + g1),M) by Th31;

      (f + g) in ( L1_Functions M) & (f1 + g1) in ( L1_Functions M) by A1, Th23;

      hence thesis by A3, Th39;

    end;

    theorem :: LPSPACE1:42

    

     Th42: 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 that

       A1: f in ( L1_Functions M) & g in ( L1_Functions M) and

       A2: ( a.e-eq-class (f,M)) = ( a.e-eq-class (g,M));

      f a.e.= (g,M) by A1, A2, Th39;

      then

       A3: (a (#) f) a.e.= ((a (#) g),M) by Th32;

      (a (#) f) in ( L1_Functions M) & (a (#) g) in ( L1_Functions M) by A1, Th24;

      hence thesis by A3, Th39;

    end;

    definition

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

      :: LPSPACE1:def14

      func CosetSet M -> non empty Subset-Family of ( L1_Functions M) equals { ( a.e-eq-class (f,M)) where f be PartFunc of X, REAL : f in ( L1_Functions M) };

      correctness

      proof

        set C = { ( a.e-eq-class (f,M)) where f be PartFunc of X, REAL : f in ( L1_Functions M) };

        

         A1: C c= ( bool ( L1_Functions M))

        proof

          let x be object;

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

        end;

        (X --> 0 ) in ( L1_Functions M) by Lm3;

        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;

      :: LPSPACE1:def15

      func addCoset M -> BinOp of ( CosetSet M) means

      : Def15: 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

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

        set C = ( CosetSet 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)) and

           A3: a in ( L1_Functions M);

          B in C;

          then

          consider b be PartFunc of X, REAL such that

           A4: B = ( a.e-eq-class (b,M)) and

           A5: b in ( L1_Functions M);

          set z = ( a.e-eq-class ((a + b),M));

          

           A6: (a + b) in ( L1_Functions M) by A3, A5, Th23;

          then z in C;

          then

          reconsider z as Element of C;

          take z;

          now

            let a1,b1 be PartFunc of X, REAL ;

            assume

             A7: a1 in A & b1 in B;

            then a1 a.e.= (a,M) & b1 a.e.= (b,M) by A2, A3, A4, A5, Th37;

            then

             A8: (a1 + b1) a.e.= ((a + b),M) by Th31;

            (a1 + b1) in ( L1_Functions M) by A7, Th23;

            hence z = ( a.e-eq-class ((a1 + b1),M)) by A6, A8, Th39;

          end;

          hence P[A, B, z];

        end;

        consider f be Function of [:C, C:], C such that

         A9: 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 thesis by A9;

      end;

      uniqueness

      proof

        set C = ( CosetSet M);

        let f1,f2 be BinOp of ( CosetSet M) such that

         A10: 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

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

        now

          let A,B be Element of ( CosetSet M);

          A in C;

          then

          consider a1 be PartFunc of X, REAL such that

           A12: 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

           A13: B = ( a.e-eq-class (b1,M)) & b1 in ( L1_Functions M);

          

           A14: b1 in B by A13, Th38;

          

           A15: a1 in A by A12, Th38;

          then (f1 . (A,B)) = ( a.e-eq-class ((a1 + b1),M)) by A10, A14;

          hence (f1 . (A,B)) = (f2 . (A,B)) by A11, A15, A14;

        end;

        hence thesis;

      end;

    end

    definition

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

      :: LPSPACE1:def16

      func zeroCoset M -> Element of ( CosetSet M) means

      : Def16: 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 Lm3;

        then ( a.e-eq-class ((X --> 0 ),M)) in ( CosetSet M);

        hence thesis by Lm3;

      end;

    end

    definition

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

      :: LPSPACE1:def17

      func lmultCoset M -> Function of [: REAL , ( CosetSet M):], ( CosetSet M) means

      : Def17: for z be 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

        defpred P[ Real, set, set] means for f be PartFunc of X, REAL st f in $2 holds $3 = ( a.e-eq-class (($1 (#) f),M));

        set C = ( CosetSet 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)) and

           A3: a in ( L1_Functions M);

          set c = ( a.e-eq-class ((z (#) a),M));

          

           A4: (z (#) a) in ( L1_Functions M) by A3, Th24;

          then c in C;

          then

          reconsider c as Element of C;

          take c;

          now

            let a1 be PartFunc of X, REAL ;

            assume

             A5: a1 in A;

            then a1 a.e.= (a,M) by A2, A3, Th37;

            then

             A6: (z (#) a1) a.e.= ((z (#) a),M) by Th32;

            (z (#) a1) in ( L1_Functions M) by A5, Th24;

            hence c = ( a.e-eq-class ((z (#) a1),M)) by A4, A6, Th39;

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

        

         A8: for z be Real, A be Element of C holds P[z, A, (f . (z,A))]

        proof

          let z be Real, A be Element of C;

          reconsider z as Element of REAL by XREAL_0:def 1;

           P[z, A, (f . (z,A))] by A7;

          hence thesis;

        end;

        take f;

        let z be Real, A be Element of C, a be PartFunc of X, REAL ;

        assume a in A;

        hence thesis by A8;

      end;

      uniqueness

      proof

        set C = ( CosetSet M);

        let f1,f2 be Function of [: REAL , C:], C such that

         A9: for z be 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

         A10: for z be 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

           A11: A = ( a.e-eq-class (a1,M)) & a1 in ( L1_Functions M);

          

          thus (f1 . (z,A)) = ( a.e-eq-class ((z (#) a1),M)) by A9, A11, Th38

          .= (f2 . (z,A)) by A10, A11, Th38;

        end;

        hence thesis;

      end;

    end

    definition

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

      :: LPSPACE1:def18

      func Pre-L-Space M -> strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct means

      : Def18: 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

           A3: A2 = ( a.e-eq-class (b,M)) & b in ( L1_Functions M);

          

           A4: b in A2 by A3, Th38;

          

           A5: a in A1 by A2, Th38;

          then (A1 + A2) = ( a.e-eq-class ((a + b),M)) by A4, Def15;

          hence thesis by A5, A4, Def15;

        end;

        

         A6: A is right_zeroed

        proof

          consider z be PartFunc of X, REAL such that

           A7: z = (X --> 0 ) and

           A8: z in ( L1_Functions M) and

           A9: ( zeroCoset M) = ( a.e-eq-class (z,M)) by Def16;

          

           A10: z in ( 0. A) by A8, A9, Th38;

          let A1 be Element of A;

          A1 in C;

          then

          consider a be PartFunc of X, REAL such that

           A11: A1 = ( a.e-eq-class (a,M)) and

           A12: a in ( L1_Functions M);

          reconsider a1 = a, z1 = z as VECTOR of ( RLSp_L1Funct M) by A12, A8;

          

           A13: (a + z) = (a1 + z1) by Th25

          .= (a1 + ( 0. ( RLSp_L1Funct M))) by A7

          .= a by RLVECT_1:def 4;

          a in A1 by A11, A12, Th38;

          hence thesis by A11, A10, A13, Def15;

        end;

         A14:

        now

          let x,y be Real, A1,A2 be Element of A;

          reconsider x1 = x, y1 = y as Real;

          A1 in C;

          then

          consider a be PartFunc of X, REAL such that

           A15: A1 = ( a.e-eq-class (a,M)) and

           A16: a in ( L1_Functions M);

          

           A17: a in A1 by A15, A16, Th38;

          then (lC . (x1,A1)) = ( a.e-eq-class ((x (#) a),M)) by Def17;

          then

           A18: (x (#) a) in (x * A1) by A16, Th24, Th38;

          A2 in C;

          then

          consider b be PartFunc of X, REAL such that

           A19: A2 = ( a.e-eq-class (b,M)) and

           A20: b in ( L1_Functions M);

          reconsider a1 = a, b1 = b as VECTOR of ( RLSp_L1Funct M) by A16, A20;

          

           A21: (x (#) a) = (x1 * a1) by Th26;

          

           A22: b in A2 by A19, A20, Th38;

          then (lC . (x1,A2)) = ( a.e-eq-class ((x (#) b),M)) by Def17;

          then

           A23: (x (#) b) in (x1 * A2) by A20, Th24, Th38;

          (a + b) = (a1 + b1) by Th25;

          then (x (#) (a + b)) = (x1 * (a1 + b1)) by Th26;

          then

           A24: (x (#) (a + b)) = ((x * a1) + (x * b1)) by RLVECT_1:def 5;

          (x (#) b) = (x1 * b1) by Th26;

          then

           A25: (x (#) (a + b)) = ((x (#) a) + (x (#) b)) by A21, A24, Th25;

          (aC . (A1,A2)) = ( a.e-eq-class ((a + b),M)) by A17, A22, Def15;

          then (a + b) in (A1 + A2) by A16, A20, Th23, Th38;

          then (x1 * (A1 + A2)) = ( a.e-eq-class (((x (#) a) + (x (#) b)),M)) by A25, Def17;

          hence (x * (A1 + A2)) = ((x * A1) + (x * A2)) by A18, A23, Def15;

          

           A26: (y (#) a) = (y1 * a1) by Th26;

          (lC . (y1,A1)) = ( a.e-eq-class ((y (#) a),M)) by A17, Def17;

          then

           A27: (y (#) a) in (y1 * A1) by A16, Th24, Th38;

          ((x + y) (#) a) = ((x1 + y1) * a1) by Th26

          .= ((x * a1) + (y * a1)) by RLVECT_1:def 6

          .= ((x (#) a) + (y (#) a)) by A26, A21, Th25;

          then ((x1 + y1) * A1) = ( a.e-eq-class (((x (#) a) + (y (#) a)),M)) by A17, Def17;

          hence ((x + y) * A1) = ((x * A1) + (y * A1)) by A18, A27, Def15;

          (x (#) (y (#) a)) = (x * (y * a1)) by A26, Th26

          .= ((x1 * y1) * a1) by RLVECT_1:def 7

          .= ((x * y) (#) a) by Th26;

          

          then ((x1 * y1) * A1) = ( a.e-eq-class ((x1 (#) (y1 (#) a)),M)) by A17, Def17

          .= (x * (y * A1)) by A27, Def17;

          hence ((x * y) * A1) = (x * (y * A1));

          (1 (#) a) = (1 * a1) by Th26

          .= a by RLVECT_1:def 8;

          hence (1 * A1) = A1 by A15, A17, Def17;

        end;

        

         A28: A is right_complementable

        proof

          let A1 be Element of A;

          A1 in C;

          then

          consider a be PartFunc of X, REAL such that

           A29: A1 = ( a.e-eq-class (a,M)) and

           A30: a in ( L1_Functions M);

          set A2 = ( a.e-eq-class ((( - 1) (#) a),M));

          

           A31: (( - 1) (#) a) in ( L1_Functions M) by A30, Th24;

          then A2 in C;

          then

          reconsider A2 as Element of A;

          

           A32: a in A1 & (( - 1) (#) a) in A2 by A29, A30, Th24, Th38;

          reconsider a1 = a as VECTOR of ( RLSp_L1Funct M) by A30;

          take A2;

          consider v,g be PartFunc of X, REAL such that v in ( L1_Functions M) and g in ( L1_Functions M) and

           A33: v = (a1 + (( - 1) * a1)) and

           A34: g = (X --> 0 ) and

           A35: v a.e.= (g,M) by Th27;

          

           A36: 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 Def16;

          

           A37: (a + (( - 1) (#) a)) in ( L1_Functions M) by A30, A31, Th23;

          (( - 1) (#) a) = (( - 1) * a1) by Th26;

          then (a + (( - 1) (#) a)) a.e.= (g,M) by A33, A35, Th25;

          then ( 0. A) = ( a.e-eq-class ((a + (( - 1) (#) a)),M)) by A34, A37, A36, Th39;

          hence thesis by A32, Def15;

        end;

        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

           A38: A1 = ( a.e-eq-class (a,M)) and

           A39: a in ( L1_Functions M);

          A2 in C;

          then

          consider b be PartFunc of X, REAL such that

           A40: A2 = ( a.e-eq-class (b,M)) and

           A41: b in ( L1_Functions M);

          A3 in C;

          then

          consider c be PartFunc of X, REAL such that

           A42: A3 = ( a.e-eq-class (c,M)) and

           A43: c in ( L1_Functions M);

          

           A44: c in A3 by A42, A43, Th38;

          

           A45: b in A2 by A40, A41, Th38;

          then (aC . (A2,A3)) = ( a.e-eq-class ((b + c),M)) by A44, Def15;

          then

           A46: (b + c) in (A2 + A3) by A41, A43, Th23, Th38;

          reconsider a1 = a, b1 = b, c1 = c as VECTOR of ( RLSp_L1Funct M) by A39, A41, A43;

          (b + c) = (b1 + c1) by Th25;

          then (a + (b + c)) = (a1 + (b1 + c1)) by Th25;

          then

           A47: (a + (b + c)) = ((a1 + b1) + c1) by RLVECT_1:def 3;

          (a + b) = (a1 + b1) by Th25;

          then

           A48: (a + (b + c)) = ((a + b) + c) by A47, Th25;

          

           A49: a in A1 by A38, A39, Th38;

          then (aC . (A1,A2)) = ( a.e-eq-class ((a + b),M)) by A45, Def15;

          then (a + b) in (A1 + A2) by A39, A41, Th23, Th38;

          then ((A1 + A2) + A3) = ( a.e-eq-class ((a + (b + c)),M)) by A44, A48, Def15;

          hence thesis by A49, A46, Def15;

        end;

        then

        reconsider A as strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct by A1, A6, A28, A14, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

        take A;

        thus thesis;

      end;

      uniqueness ;

    end

    begin

    theorem :: LPSPACE1:43

    

     Th43: f in ( L1_Functions M) & g in ( L1_Functions M) & f a.e.= (g,M) implies ( Integral (M,f)) = ( Integral (M,g))

    proof

      assume that

       A1: f in ( L1_Functions M) and

       A2: g in ( L1_Functions M) and

       A3: f a.e.= (g,M);

      consider EQ be Element of S such that

       A4: (M . EQ) = 0 and

       A5: (f | (EQ ` )) = (g | (EQ ` )) by A3;

      

       A6: 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

       A7: (M . NDf) = 0 and

       A8: ( dom f) = (NDf ` ) and f is_integrable_on M;

      

       A9: (M . (EQ \/ NDf)) = 0 by A7, A4, Lm4;

      ( R_EAL f) is_integrable_on M by A6;

      then

      consider E1 be Element of S such that

       A10: E1 = ( dom ( R_EAL f)) and

       A11: ( R_EAL f) is E1 -measurable;

      

       A12: f is E1 -measurable by A11;

      

       A13: 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 A2;

      then

      consider NDg be Element of S such that

       A14: (M . NDg) = 0 and

       A15: ( dom g) = (NDg ` ) and g is_integrable_on M;

      

       A16: (M . (EQ \/ NDg)) = 0 by A14, A4, Lm4;

      ( R_EAL g) is_integrable_on M by A13;

      then

      consider E2 be Element of S such that

       A17: E2 = ( dom ( R_EAL g)) and

       A18: ( R_EAL g) is E2 -measurable;

      

       A19: g is E2 -measurable by A18;

      

       A20: ((EQ ` ) \ (NDf \/ NDg)) = ((EQ \/ (NDf \/ NDg)) ` ) by XBOOLE_1: 41

      .= ((NDg \/ (EQ \/ NDf)) ` ) by XBOOLE_1: 4

      .= ((NDg ` ) \ (EQ \/ NDf)) by XBOOLE_1: 41;

      

       A21: ((EQ ` ) \ (NDf \/ NDg)) = ((EQ \/ (NDf \/ NDg)) ` ) by XBOOLE_1: 41

      .= ((NDf \/ (EQ \/ NDg)) ` ) by XBOOLE_1: 4

      .= ((NDf ` ) \ (EQ \/ NDg)) by XBOOLE_1: 41;

      

       A22: ((EQ ` ) \ (NDf \/ NDg)) c= (EQ ` ) by XBOOLE_1: 36;

      

      then (f | ((EQ ` ) \ (NDf \/ NDg))) = ((g | (EQ ` )) | ((EQ ` ) \ (NDf \/ NDg))) by A5, FUNCT_1: 51

      .= (g | ((EQ ` ) \ (NDf \/ NDg))) by A22, FUNCT_1: 51;

      

      hence ( Integral (M,f)) = ( Integral (M,(g | ((NDg ` ) \ (EQ \/ NDf))))) by A8, A10, A12, A21, A20, A16, MESFUNC6: 89

      .= ( Integral (M,g)) by A15, A17, A19, A9, MESFUNC6: 89;

    end;

    theorem :: LPSPACE1:44

    

     Th44: 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;

      then

      consider A be Element of S such that

       A3: A = ( dom ( R_EAL f)) and

       A4: ( R_EAL f) is A -measurable;

      

       A5: f is A -measurable by A4;

      then ( abs f) is_integrable_on M by A1, A3, MESFUNC6: 94;

      then -infty < ( Integral (M,( abs f))) & ( Integral (M,( abs f))) < +infty by MESFUNC6: 90;

      hence thesis by A1, A2, A3, A5, MESFUNC6: 94, XXREAL_0: 14;

    end;

    theorem :: LPSPACE1:45

    

     Th45: 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) and

       A2: g in ( L1_Functions M) and

       A3: f a.e.= (g,M);

      

       A4: 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

       A5: (M . NDf) = 0 and

       A6: ( dom f) = (NDf ` ) and f is_integrable_on M;

      

       A7: ( abs f) is_integrable_on M by A4, Th44;

      consider EQ be Element of S such that

       A8: (M . EQ) = 0 and

       A9: (f | (EQ ` )) = (g | (EQ ` )) by A3;

      (( abs f) | (EQ ` )) = ( abs (g | (EQ ` ))) by A9, RFUNCT_1: 46

      .= (( abs g) | (EQ ` )) by RFUNCT_1: 46;

      then

       A10: ( abs f) a.e.= (( abs g),M) by A8;

      

       A11: 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 A2;

      then

      consider NDg be Element of S such that

       A12: (M . NDg) = 0 and

       A13: ( dom g) = (NDg ` ) and g is_integrable_on M;

      

       A14: ( abs g) is_integrable_on M by A11, Th44;

      ( dom ( abs g)) = (NDg ` ) by A13, VALUED_1:def 11;

      then

       A15: ( abs g) in ( L1_Functions M) by A12, A14;

      ( dom ( abs f)) = (NDf ` ) by A6, VALUED_1:def 11;

      then ( abs f) in ( L1_Functions M) by A5, A7;

      hence thesis by A15, A10, Th43;

    end;

    theorem :: LPSPACE1:46

    

     Th46: (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 and

       A2: g in x;

      x in the carrier of ( Pre-L-Space M);

      then x in ( CosetSet M) by Def18;

      then

      consider h be PartFunc of X, REAL such that

       A3: x = ( a.e-eq-class (h,M)) and h in ( L1_Functions M);

      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, A3;

      then

       A4: f a.e.= (h,M);

      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 A2, A3;

      hence thesis by A1, A3, A4, Th30;

    end;

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

    theorem :: LPSPACE1:47

    

     Th47: f in x implies f is_integrable_on M & f in ( L1_Functions M) & ( abs f) is_integrable_on M

    proof

      x in the carrier of ( Pre-L-Space M);

      then x in ( CosetSet M) by Def18;

      then

      consider h be PartFunc of X, REAL such that

       A1: x = ( a.e-eq-class (h,M)) and h in ( L1_Functions M);

      assume f in x;

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

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

    end;

    theorem :: LPSPACE1:48

    

     Th48: 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 that

       A1: f in x and

       A2: g in x;

      

       A3: g in ( L1_Functions M) by A2, Th46;

      f a.e.= (g,M) & f in ( L1_Functions M) by A1, A2, Th46;

      hence thesis by A3, Th43, Th45;

    end;

    definition

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

      :: LPSPACE1:def19

      func L-1-Norm M -> Function of the carrier of ( Pre-L-Space M), REAL means

      : Def19: for x be Point of ( Pre-L-Space M) holds ex f be PartFunc of X, REAL st f in x & (it . x) = ( Integral (M,( abs f)));

      existence

      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) holds ex y be 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 Def18;

          then

          consider f be PartFunc of X, REAL such that

           A2: x = ( a.e-eq-class (f,M)) and

           A3: 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 A3;

          then ( Integral (M,( abs f))) in REAL by Th44;

          hence thesis by A2, A3, Th38;

        end;

        consider f be Function of ( Pre-L-Space M), REAL such that

         A4: for x be Point of ( Pre-L-Space M) holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let N1,N2 be Function of the carrier of ( Pre-L-Space M), REAL ;

        assume

         A5: (for x be Point of ( Pre-L-Space M) holds 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) holds 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 A5;

          hence (N1 . x) = (N2 . x) by Th48;

        end;

        hence N1 = N2 by FUNCT_2: 63;

      end;

    end

    definition

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

      :: LPSPACE1:def20

      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 :: LPSPACE1:49

    

     Th49: (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 and

       A2: (( L-1-Norm M) . y) = ( Integral (M,( abs f))) by Def19;

      y in the carrier of ( Pre-L-Space M);

      then y in ( CosetSet M) by Def18;

      then

      consider g be PartFunc of X, REAL such that

       A3: y = ( a.e-eq-class (g,M)) & g in ( L1_Functions M);

      g in y by A3, Th38;

      then f a.e.= (g,M) by A1, Th46;

      then x = ( a.e-eq-class (f,M)) by A1, A3, Th39;

      hence thesis by A1, A2, Th48;

    end;

    theorem :: LPSPACE1:50

    

     Th50: 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 Def18;

      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, Th38;

      then f a.e.= (g,M) by A1, Th46;

      hence thesis by A1, A2, Th39, Th49;

    end;

    theorem :: LPSPACE1:51

    

     Th51: (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

        reconsider x1 = x, y1 = y as Point of ( Pre-L-Space M);

        assume that

         A1: f in x and

         A2: g in y;

        y1 in the carrier of ( Pre-L-Space M);

        then

         A3: y1 in C by Def18;

        then

        consider b be PartFunc of X, REAL such that

         A4: y1 = ( a.e-eq-class (b,M)) and

         A5: b in ( L1_Functions M);

        

         A6: b in y1 by A4, A5, Th38;

        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, A4;

        then

         A7: ( a.e-eq-class (b,M)) = ( a.e-eq-class (g,M)) by Th39;

        x1 in the carrier of ( Pre-L-Space M);

        then

         A8: x1 in C by Def18;

        then

        consider a be PartFunc of X, REAL such that

         A9: x1 = ( a.e-eq-class (a,M)) and

         A10: a in ( L1_Functions M);

        a in x1 by A9, A10, Th38;

        then (( addCoset M) . (x1,y1)) = ( a.e-eq-class ((a + b),M)) by A8, A3, A6, Def15;

        then

         A11: (x1 + y1) = ( a.e-eq-class ((a + b),M)) by Def18;

        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 A1, A9;

        then ( a.e-eq-class (a,M)) = ( a.e-eq-class (f,M)) by Th39;

        then ( a.e-eq-class ((a + b),M)) = ( a.e-eq-class ((f + g),M)) by A1, A2, A9, A10, A4, A5, A7, Th41;

        hence (f + g) in (x + y) by A1, A2, A9, A4, A11, Th23, Th38;

      end;

      hereby

        reconsider x1 = x as Point of ( Pre-L-Space M);

        x1 in the carrier of ( Pre-L-Space M);

        then

         A12: x1 in C by Def18;

        then

        consider f1 be PartFunc of X, REAL such that

         A13: x1 = ( a.e-eq-class (f1,M)) and

         A14: f1 in ( L1_Functions M);

        f1 in x1 by A13, A14, Th38;

        then (( lmultCoset M) . (a,x1)) = ( a.e-eq-class ((a (#) f1),M)) by A12, Def17;

        then

         A15: (a * x1) = ( a.e-eq-class ((a (#) f1),M)) by Def18;

        assume

         A16: f in x;

        then 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 A13;

        then ( a.e-eq-class (f1,M)) = ( a.e-eq-class (f,M)) by Th39;

        then ( a.e-eq-class ((a (#) f1),M)) = ( a.e-eq-class ((a (#) f),M)) by A16, A13, A14, Th42;

        hence (a (#) f) in (a * x) by A16, A13, A15, Th24, Th38;

      end;

    end;

    theorem :: LPSPACE1:52

    

     Th52: E = ( dom f) & (for x be set st x in ( dom f) holds (f . x) = r) implies f is E -measurable

    proof

      assume

       A1: E = ( dom f);

      r in REAL by XREAL_0:def 1;

      then

      reconsider r0 = r as R_eal by NUMBERS: 31;

      set g = ( R_EAL f);

      consider g0 be PartFunc of X, ExtREAL such that

       A2: g0 is_simple_func_in S and

       A3: ( dom g0) = E and

       A4: for x be object st x in E holds (g0 . x) = r0 by MESFUNC5: 41;

      assume

       A5: for x be set st x in ( dom f) holds (f . x) = r;

      now

        let x be Element of X;

        assume

         A6: x in ( dom g);

        then (g . x) = r by A5;

        hence (g . x) = (g0 . x) by A1, A4, A6;

      end;

      then g0 = g by A1, A3, PARTFUN1: 5;

      then g is E -measurable by A2, MESFUNC2: 34;

      hence thesis;

    end;

    theorem :: LPSPACE1:53

    

     Th53: f in ( L1_Functions M) & ( Integral (M,( abs f))) = 0 implies f a.e.= ((X --> 0 ),M)

    proof

      assume that

       A1: f in ( L1_Functions M) and

       A2: ( Integral (M,( abs f))) = 0 ;

      set g = (X --> 0 );

      defpred P[ Element of NAT , set] means $2 = ( great_eq_dom (( abs f),(1 / ($1 + 1)))) & (M . $2) = 0 ;

      consider f1 be PartFunc of X, REAL such that

       A3: f = f1 and

       A4: ex ND be Element of S st (M . ND) = 0 & ( dom f1) = (ND ` ) & f1 is_integrable_on M by A1;

      

       A5: ( abs f) is_integrable_on M by A3, A4, Th44;

      then ( R_EAL ( abs f)) is_integrable_on M;

      then

      consider E be Element of S such that

       A6: E = ( dom ( R_EAL ( abs f))) and

       A7: ( R_EAL ( abs f)) is E -measurable;

      

       A8: ( abs f) is E -measurable by A7;

      now

        let x be object;

        assume x in ( dom ( abs f));

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

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

      end;

      then

       A9: ( abs f) is nonnegative by MESFUNC6: 52;

       A10:

      now

        let n be Element of NAT ;

        reconsider r = (1 / (n + 1)) as Element of REAL by XREAL_0:def 1;

        reconsider Br = (E /\ ( great_eq_dom (( abs f),r))) as Element of S by A6, A8, MESFUNC6: 13;

        set g = (Br --> r);

        

         A11: ( dom g) = Br by FUNCT_2:def 1;

        

         A12: for x be set st x in ( dom g) holds (g . x) = r by FUNCOP_1: 7;

        reconsider g as PartFunc of X, REAL by RELSET_1: 7;

        

         A13: (( abs f) | Br) is_integrable_on M by A5, MESFUNC6: 91;

        for x be object st x in ( dom g) holds 0 <= (g . x) by A12;

        then g is nonnegative by MESFUNC6: 52;

        then

         A14: 0 <= ( Integral (M,g)) by A11, A12, Th52, MESFUNC6: 84;

        

         A15: ( dom ( abs g)) = ( dom g) by VALUED_1:def 11;

         A16:

        now

          let x be Element of X;

          assume

           A17: x in ( dom ( abs g));

          then (( abs g) . x) = |.(g . x) qua Complex.| by VALUED_1:def 11;

          then (( abs g) . x) = |.r qua Complex.| by A12, A15, A17;

          then (( abs g) . x) = r by ABSVALUE:def 1;

          hence (( abs g) . x) = (g . x) by A12, A15, A17;

        end;

        

         A18: ( dom (( abs f) | Br)) = (( dom ( abs f)) /\ Br) by RELAT_1: 61

        .= Br by A6, XBOOLE_1: 17, XBOOLE_1: 28;

        then

         A19: ( dom g) = ( dom (( abs f) | Br)) by FUNCT_2:def 1;

         A20:

        now

          let x be Element of X;

          assume

           A21: x in ( dom g);

          then x in (E /\ ( great_eq_dom (( abs f),r))) by FUNCT_2:def 1;

          then x in ( great_eq_dom (( abs f),r)) by XBOOLE_0:def 4;

          then

           A22: ex y be Real st y = (( abs f) . x) & r <= y by MESFUNC6: 6;

           |.(g . x) qua Complex.| = |.r qua Complex.| by A12, A21;

          then |.(g . x) qua Complex.| = r by ABSVALUE:def 1;

          hence |.(g . x) qua Complex.| <= ((( abs f) | Br) . x) by A19, A21, A22, FUNCT_1: 47;

        end;

        g is Br -measurable by A11, A12, Th52;

        then ( Integral (M,( abs g))) <= ( Integral (M,(( abs f) | Br))) by A11, A18, A13, A20, MESFUNC6: 96;

        then

         A23: ( Integral (M,g)) <= ( Integral (M,(( abs f) | Br))) by A15, A16, PARTFUN1: 5;

        

         A24: for x be object st x in ( dom g) holds (g . x) = r by A11, FUNCOP_1: 7;

        reconsider rr = r as R_eal;

        ( Integral (M,(( abs f) | Br))) <= ( Integral (M,(( abs f) | E))) by A6, A8, A9, MESFUNC6: 87, XBOOLE_1: 17;

        then ( Integral (M,g)) = 0 by A2, A6, A23, A14, RELAT_1: 68;

        then (rr * (M . Br)) = 0 by A11, A24, MESFUNC6: 97;

        then

         A25: (M . Br) = 0 ;

        for x be object st x in ( great_eq_dom (( abs f),r)) holds x in ( dom ( abs f)) by MESFUNC6: 6;

        then ( great_eq_dom (( abs f),r)) c= E by A6;

        hence ex B be Element of S st P[n, B] by A25, XBOOLE_1: 28;

      end;

      consider F be sequence of S such that

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

      now

        let y be object;

        assume y in ( union ( rng F));

        then

        consider B be set such that

         A27: y in B and

         A28: B in ( rng F) by TARSKI:def 4;

        consider n be object such that

         A29: n in NAT and

         A30: B = (F . n) by A28, FUNCT_2: 11;

        reconsider m = n as Element of NAT by A29;

        

         A31: y in ( great_eq_dom (( abs f),(1 / (m + 1)))) by A26, A27, A30;

        then

         A32: y in ( dom ( abs f)) by MESFUNC6: 6;

        then

         A33: y in ( dom f) by VALUED_1:def 11;

        

         A34: (( abs f) . y) = |.(f . y) qua Complex.| by A32, VALUED_1:def 11;

        (( abs f) . y) <> 0 by A31, MESFUNC1:def 14;

        then (f . y) <> 0 by A34, ABSVALUE: 2;

        hence y in { x where x be Element of X : x in ( dom f) & (f . x) <> 0 } by A33;

      end;

      then

       A35: ( union ( rng F)) c= { x where x be Element of X : x in ( dom f) & (f . x) <> 0 };

      consider ND be Element of S such that

       A36: (M . ND) = 0 and

       A37: ( dom f1) = (ND ` ) and f1 is_integrable_on M by A4;

      reconsider EQ = (( union ( rng F)) \/ ND) as Element of S;

      

       A38: (EQ ` ) = ((ND ` ) /\ (( union ( rng F)) ` )) by XBOOLE_1: 53;

      then

       A39: (EQ ` ) c= ( dom f) by A3, A37, XBOOLE_1: 17;

      ( dom g) = X by FUNCOP_1: 13;

      then

       A40: ( dom (g | (EQ ` ))) = (EQ ` ) by RELAT_1: 62;

      

       A41: ( dom (f | (EQ ` ))) = (EQ ` ) by A3, A37, A38, RELAT_1: 62, XBOOLE_1: 17;

      now

        let y be object;

        assume y in { x where x be Element of X : x in ( dom f) & (f . x) <> 0 };

        then

        consider z be Element of X such that

         A42: y = z and

         A43: z in ( dom f) and

         A44: (f . z) <> 0 ;

        

         A45: z in ( dom ( abs f)) by A43, VALUED_1:def 11;

        then (( abs f) . z) = |.(f . z) qua Complex.| by VALUED_1:def 11;

        then 0 < (( abs f) . z) by A44, COMPLEX1: 47;

        then

        consider n be Element of NAT such that

         A46: (1 / (n + 1)) < ((( abs f) . z) - 0 ) by MESFUNC1: 10;

        z in ( great_eq_dom (( abs f),(1 / (n + 1)))) by A45, A46, MESFUNC6: 6;

        then

         A47: y in (F . n) by A26, A42;

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

        hence y in ( union ( rng F)) by A47, TARSKI:def 4;

      end;

      then { x where x be Element of X : x in ( dom f) & (f . x) <> 0 } c= ( union ( rng F));

      then

       A48: { x where x be Element of X : x in ( dom f) & (f . x) <> 0 } = ( union ( rng F)) by A35, XBOOLE_0:def 10;

       A49:

      now

        let x be set;

        assume

         A50: x in (EQ ` );

        then x in (( union ( rng F)) ` ) by A38, XBOOLE_0:def 4;

        then not x in ( union ( rng F)) by XBOOLE_0:def 5;

        hence (f . x) = 0 by A48, A39, A50;

      end;

      now

        let y be object;

        assume

         A51: y in ( dom (f | (EQ ` )));

        then ((f | (EQ ` )) . y) = (f . y) by FUNCT_1: 47;

        then ((f | (EQ ` )) . y) = 0 by A41, A49, A51;

        then ((f | (EQ ` )) . y) = (g . y) by A51, FUNCOP_1: 7;

        hence ((f | (EQ ` )) . y) = ((g | (EQ ` )) . y) by A41, A40, A51, FUNCT_1: 47;

      end;

      then

       A52: (f | (EQ ` )) = (g | (EQ ` )) by A39, A40, FUNCT_1: 2, RELAT_1: 62;

      now

        let A be set;

        assume A in ( rng F);

        then

        consider n be object such that

         A53: n in NAT and

         A54: A = (F . n) by FUNCT_2: 11;

        reconsider n as Element of NAT by A53;

        (M . (F . n)) = 0 by A26;

        hence A is measure_zero of M by A54, MEASURE1:def 7;

      end;

      then

       A55: ( union ( rng F)) is measure_zero of M by MEASURE2: 14;

      ND is measure_zero of M by A36, MEASURE1:def 7;

      then EQ is measure_zero of M by A55, MEASURE1: 37;

      then (M . EQ) = 0 by MEASURE1:def 7;

      hence thesis by A52;

    end;

    theorem :: LPSPACE1:54

    

     Th54: ( Integral (M,( abs (X --> 0 )))) = 0

    proof

      set f = (X --> 0 );

       A1:

      now

        let x be Element of X;

        (f . x) = 0 by FUNCOP_1: 7;

        then

         A2: |.(f . x) qua Complex.| = 0 by ABSVALUE: 2;

        assume x in ( dom ( abs f));

        hence (( abs f) . x) = 0 by A2, VALUED_1:def 11;

      end;

      ( dom f) = X by FUNCOP_1: 13;

      then ( dom ( abs f)) = X by VALUED_1:def 11;

      hence thesis by A1, Lm2;

    end;

    theorem :: LPSPACE1:55

    

     Th55: 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 that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      

       A3: f1 is_integrable_on M by A1;

      then

      consider B be Element of S such that

       A4: B = ( dom f1) and f1 is B -measurable;

      

       A5: B = ( dom |.f1.|) by A4, MESFUNC1:def 10;

       |.f1.| is_integrable_on M by A3, MESFUNC5: 100;

      then

       A6: ex E be Element of S st E = ( dom |.f1.|) & |.f1.| is E -measurable;

      

       A7: g1 is_integrable_on M by A2;

      then

      consider C be Element of S such that

       A8: C = ( dom g1) and g1 is C -measurable;

      

       A9: C = ( dom |.g1.|) by A8, MESFUNC1:def 10;

      consider E be Element of S such that

       A10: E = ( dom (f1 + g1)) and

       A11: ( Integral (M,( |.(f1 + g1).| | E))) <= (( Integral (M,( |.f1.| | E))) + ( Integral (M,( |.g1.| | E)))) by A3, A7, MESFUNC7: 22;

      ( dom |.(f1 + g1).|) = E by A10, MESFUNC1:def 10;

      then (f1 + g1) = ( R_EAL (f + g)) & ( |.(f1 + g1).| | E) = |.(f1 + g1).| by MESFUNC6: 23, RELAT_1: 68;

      then

       A12: ( Integral (M,( |.(f1 + g1).| | E))) = ( Integral (M, |.(f + g).|)) by MESFUNC6: 1;

       |.g1.| is_integrable_on M by A7, MESFUNC5: 100;

      then

       A13: ex E be Element of S st E = ( dom |.g1.|) & |.g1.| is E -measurable;

      

       A14: E = ((( dom f1) /\ ( dom g1)) \ (((f1 " { -infty }) /\ (g1 " { +infty })) \/ ((f1 " { +infty }) /\ (g1 " { -infty })))) by A10, MESFUNC1:def 3;

      then E c= ( dom g1) by XBOOLE_1: 18, XBOOLE_1: 36;

      then E c= ( dom |.g1.|) by MESFUNC1:def 10;

      then ( Integral (M,( |.g1.| | E))) <= ( Integral (M,( |.g1.| | C))) by A9, A13, MESFUNC5: 93;

      then ( Integral (M,( |.g1.| | E))) <= ( Integral (M, |.g1.|)) by A9, RELAT_1: 68;

      then

       A15: ( Integral (M,( |.g1.| | E))) <= ( Integral (M, |.g.|)) by MESFUNC6: 1;

      E c= ( dom f1) by A14, XBOOLE_1: 18, XBOOLE_1: 36;

      then E c= ( dom |.f1.|) by MESFUNC1:def 10;

      then ( Integral (M,( |.f1.| | E))) <= ( Integral (M,( |.f1.| | B))) by A5, A6, MESFUNC5: 93;

      then ( Integral (M,( |.f1.| | E))) <= ( Integral (M, |.f1.|)) by A5, RELAT_1: 68;

      then ( Integral (M,( |.f1.| | E))) <= ( Integral (M, |.f.|)) by MESFUNC6: 1;

      then (( Integral (M,( |.f1.| | E))) + ( Integral (M,( |.g1.| | E)))) <= (( Integral (M, |.f.|)) + ( Integral (M, |.g.|))) by A15, XXREAL_3: 36;

      hence thesis by A11, A12, XXREAL_0: 2;

    end;

    

     Lm7: ( L-1-Space M) is RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable

    proof

      now

        let x,y be Point of ( L-1-Space M), a be Real;

        consider f be PartFunc of X, REAL such that

         A1: f in x and

         A2: ||.x.|| = ( Integral (M,( abs f))) by Def19;

        ( abs f) is_integrable_on M by A1, Th47;

        then ( Integral (M,( |.a qua Complex.| (#) ( abs f)))) = ( |.a qua Complex.| * ( Integral (M,( abs f)))) by MESFUNC6: 102;

        then ( Integral (M,( abs (a (#) f)))) = ( |.a qua Complex.| * ( Integral (M,( abs f)))) by RFUNCT_1: 25;

        then

         A3: ( Integral (M,( abs (a (#) f)))) = ( |.a qua Complex.| * ||.x.||) by A2, EXTREAL1: 1;

        hereby

          set g = (X --> 0 );

          reconsider x1 = x as Point of ( Pre-L-Space M);

          consider f be PartFunc of X, REAL such that

           A4: f in x1 and (( L-1-Norm M) . x1) = ( Integral (M,( abs f))) by Def19;

          

           A5: f in ( L1_Functions M) by A4, Th47;

          then

           A6: ( a.e-eq-class (f,M)) in ( CosetSet M);

          

           A7: g in ( L1_Functions M) by Lm3;

          assume ||.x.|| = 0 ;

          then ( Integral (M,( abs f))) = 0 by A4, Th49;

          then f a.e.= (g,M) by A5, Th53;

          then ( a.e-eq-class (g,M)) = ( a.e-eq-class (f,M)) by A5, A7, Th39;

          then ( zeroCoset M) = ( a.e-eq-class (f,M)) by A7, A6, Def16;

          then ( 0. ( Pre-L-Space M)) = ( a.e-eq-class (f,M)) by Def18;

          hence x = ( 0. ( L-1-Space M)) by A4, Th50;

        end;

        hereby

          reconsider x1 = x as Point of ( Pre-L-Space M);

          consider f be PartFunc of X, REAL such that

           A8: f = (X --> 0 ) and

           A9: f in ( L1_Functions M) & ( zeroCoset M) = ( a.e-eq-class (f,M)) by Def16;

          assume x = ( 0. ( L-1-Space M));

          then x1 = ( 0. ( Pre-L-Space M));

          then

           A10: x1 = ( zeroCoset M) by Def18;

          (( L-1-Norm M) . x1) = ||.x.||;

          then (( L-1-Norm M) . x1) = ( Integral (M,( abs f))) by A10, A9, Th38, Th49;

          hence ||.x.|| = 0 by A8, Th54;

        end;

        

         A11: f is_integrable_on M by A1, Th47;

        then |.( Integral (M,f)).| <= ( Integral (M,( abs f))) by MESFUNC6: 95;

        hence 0 <= ||.x.|| by A2, EXTREAL1: 14;

        consider g be PartFunc of X, REAL such that

         A12: g in y and

         A13: ||.y.|| = ( Integral (M,( abs g))) by Def19;

        

         A14: g is_integrable_on M by A12, Th47;

        (f + g) in (x + y) by A1, A12, Th51;

        then

         A15: ||.(x + y).|| = ( Integral (M,( abs (f + g)))) by Th49;

        (( Integral (M,( abs f))) + ( Integral (M,( abs g)))) = ( ||.x.|| + ||.y.||) by A2, A13, SUPINF_2: 1;

        hence ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by A11, A15, A14, Th55;

        (a (#) f) in (a * x) by A1, Th51;

        hence ||.(a * x).|| = ( |.a qua Complex.| * ||.x.||) by A3, Th49;

      end;

      hence thesis by NORMSP_1:def 1, RSSPACE3: 2;

    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 vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      coherence by Lm7;

    end