lpspacc1.miz



    begin

    registration

      let D be non empty set, E be complex-membered set;

      cluster -> complex-valued for Element of ( PFuncs (D,E));

      coherence ;

    end

    definition

      let D be non empty set, E be complex-membered set, F1,F2 be Element of ( PFuncs (D,E));

      :: original: +

      redefine

      func F1 + F2 -> Element of ( PFuncs (D, COMPLEX )) ;

      coherence

      proof

        reconsider F1, F2 as PartFunc of D, E;

        (F1 + F2) is PartFunc of D, COMPLEX ;

        hence thesis by PARTFUN1: 45;

      end;

      :: original: -

      redefine

      func F1 - F2 -> Element of ( PFuncs (D, COMPLEX )) ;

      coherence

      proof

        reconsider F1, F2 as PartFunc of D, E;

        (F1 - F2) is PartFunc of D, COMPLEX ;

        hence thesis by PARTFUN1: 45;

      end;

      :: original: (#)

      redefine

      func F1 (#) F2 -> Element of ( PFuncs (D, COMPLEX )) ;

      coherence

      proof

        reconsider F1, F2 as PartFunc of D, E;

        (F1 (#) F2) is PartFunc of D, COMPLEX ;

        hence thesis by PARTFUN1: 45;

      end;

      :: original: /"

      redefine

      func F1 /" F2 -> Element of ( PFuncs (D, COMPLEX )) ;

      coherence

      proof

        reconsider F1, F2 as PartFunc of D, E;

        (F1 /" F2) is PartFunc of D, COMPLEX ;

        hence thesis by PARTFUN1: 45;

      end;

    end

    definition

      let D be non empty set, E be complex-membered set, F be Element of ( PFuncs (D,E)), a be Complex;

      :: original: (#)

      redefine

      func a (#) F -> Element of ( PFuncs (D, COMPLEX )) ;

      coherence

      proof

        reconsider F as PartFunc of D, E;

        (a (#) F) is PartFunc of D, COMPLEX ;

        hence thesis by PARTFUN1: 45;

      end;

    end

    definition

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

      :: LPSPACC1:def1

      attr V1 is multi-closed means

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

    end

    theorem :: LPSPACC1:1

    for V be ComplexLinearSpace, V1 be Subset of V holds V1 is linearly-closed iff V1 is add-closed multi-closed;

    registration

      let V be non empty CLSStruct;

      cluster add-closed multi-closed for non empty 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 CLSStruct;

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

      :: LPSPACC1:def2

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

      correctness

      proof

        

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

         A2:

        now

          let z be object;

          assume

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

          then

          consider r,x be object such that

           A4: r in COMPLEX and

           A5: x in X1 and

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

          reconsider r as Complex by A4;

          reconsider y = x as VECTOR of X by A5;

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

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

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

        end;

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

        hence thesis by A2, FUNCT_2: 3;

      end;

    end

    reserve a,b,r for Complex;

    reserve V for ComplexLinearSpace;

    theorem :: LPSPACC1:2

    

     Th2: for V be Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, V1 be non empty Subset of V, d1 be Element of V1, A be BinOp of V1, M be Function of [: COMPLEX , V1:], V1 st d1 = ( 0. V) & A = (the addF of V || V1) & M = (the Mult of V | [: COMPLEX , V1:]) holds CLSStruct (# 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 CLSStruct, V1 be non empty Subset of V, d1 be Element of V1, A be BinOp of V1, M be Function of [: COMPLEX , 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 | [: COMPLEX , V1:]);

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

       A4:

      now

        let a;

        let x be VECTOR of W;

        reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;

        

        thus (a * x) = (the Mult of V . [a1, 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 Complex;

          let x,y be VECTOR of W;

          reconsider a = a1 as Element of COMPLEX by XCMPLX_0:def 2;

          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 CLVECT_1:def 2

          .= (Av . ((Mv . (a,x)),(Mv . (a,y))))

          .= (Av . ((Mv . (a,x)),(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 Complex;

          let x be VECTOR of W;

          reconsider a = a1, b = b1 as Element of COMPLEX by XCMPLX_0:def 2;

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

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

          .= ((a + b) * y)

          .= ((a * y) + (b * y)) by CLVECT_1:def 3

          .= (Av . ((Mv . (a,y)),(Mv . (b,y))))

          .= (Av . ((Mv . (a,x)),(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 Complex;

          let x be VECTOR of W;

          reconsider a = a1, b = b1 as Element of COMPLEX by XCMPLX_0:def 2;

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

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

          .= ((a * b) * y)

          .= (a * (b * y)) by CLVECT_1:def 4

          .= (Mv . (a,(Mv . (b,y))))

          .= (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 ( 1r * x) = (Mv . ( 1r ,x)) by A4

        .= ( 1r * y)

        .= x by CLVECT_1:def 5;

      end;

      hence thesis;

    end;

    theorem :: LPSPACC1:3

    

     Th3: for V be Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, V1 be add-closed multi-closed non empty Subset of V st ( 0. V) in V1 holds CLSStruct (# 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 CLSStruct, 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;

    begin

    reserve A,B for non empty set;

    reserve f,g,h for Element of ( PFuncs (A, COMPLEX ));

    definition

      let A;

      :: LPSPACC1:def3

      func multcpfunc A -> BinOp of ( PFuncs (A, COMPLEX )) means

      : Def3: for f,g be Element of ( PFuncs (A, COMPLEX )) holds (it . (f,g)) = (f (#) g);

      existence

      proof

        deffunc F( Element of ( PFuncs (A, COMPLEX )), Element of ( PFuncs (A, COMPLEX ))) = ($1 (#) $2);

        ex F be BinOp of ( PFuncs (A, COMPLEX )) 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, COMPLEX )) 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;

      :: LPSPACC1:def4

      func multcomplexcpfunc A -> Function of [: COMPLEX , ( PFuncs (A, COMPLEX )):], ( PFuncs (A, COMPLEX )) means

      : Def4: for a be Complex, f be Element of ( PFuncs (A, COMPLEX )) holds (it . (a,f)) = (a (#) f);

      existence

      proof

        deffunc FG( Complex, Element of ( PFuncs (A, COMPLEX ))) = ($1 (#) $2);

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

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

        take F;

        let a;

        a in COMPLEX by XCMPLX_0:def 2;

        hence thesis by A1;

      end;

      uniqueness

      proof

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

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

         A3: for a be Complex, f be Element of ( PFuncs (A, COMPLEX )) holds (it2 . (a,f)) = (a (#) f);

        now

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

          

          thus (it1 . (a,f)) = (a (#) f) by A2

          .= (it2 . (a,f)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let D be non empty set;

      :: LPSPACC1:def5

      func addcpfunc (D) -> BinOp of ( PFuncs (D, COMPLEX )) means

      : Def5: for F1,F2 be Element of ( PFuncs (D, COMPLEX )) holds (it . (F1,F2)) = (F1 + F2);

      existence

      proof

        deffunc O( Element of ( PFuncs (D, COMPLEX )), Element of ( PFuncs (D, COMPLEX ))) = ($1 + $2);

        ex o be BinOp of ( PFuncs (D, COMPLEX )) st for a,b be Element of ( PFuncs (D, COMPLEX )) holds (o . (a,b)) = O(a,b) from BINOP_1:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( PFuncs (D, COMPLEX ));

        assume that

         A1: for f1,f2 be Element of ( PFuncs (D, COMPLEX )) holds (o1 . (f1,f2)) = (f1 + f2) and

         A2: for f1,f2 be Element of ( PFuncs (D, COMPLEX )) holds (o2 . (f1,f2)) = (f1 + f2);

        now

          let f1,f2 be Element of ( PFuncs (D, COMPLEX ));

          (o1 . (f1,f2)) = (f1 + f2) by A1;

          hence (o1 . (f1,f2)) = (o2 . (f1,f2)) by A2;

        end;

        hence thesis;

      end;

    end

    definition

      let A be set;

      :: LPSPACC1:def6

      func CPFuncZero A -> Element of ( PFuncs (A, COMPLEX )) equals (A --> 0c );

      coherence by PARTFUN1: 45;

    end

    definition

      let A be set;

      :: LPSPACC1:def7

      func CPFuncUnit A -> Element of ( PFuncs (A, COMPLEX )) equals (A --> 1r );

      coherence by PARTFUN1: 45;

    end

    theorem :: LPSPACC1:4

    

     Th4: h = (( addcpfunc 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 = (( addcpfunc A) . (f,g));

        then ( dom h) = ( dom (f + g)) by Def5;

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

        (h . x) = ((f + g) . x) by A1, Def5;

        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 = (( addcpfunc A) . (f,g));

       A5:

      now

        let x be Element of A;

        

         A6: (k . x) = ((f + g) . x) by Def5;

        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 Def5

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

      hence thesis by A5, PARTFUN1: 5;

    end;

    theorem :: LPSPACC1:5

    

     Th5: h = (( multcpfunc 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 = (( multcpfunc A) . (f,g));

      hereby

        assume

         A1: h = (( multcpfunc 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 :: LPSPACC1:6

    ( CPFuncZero A) <> ( CPFuncUnit A)

    proof

      (( CPFuncUnit A) . the Element of A) = 1 by COMPLEX1:def 4, FUNCOP_1: 7;

      hence thesis by FUNCOP_1: 7;

    end;

    theorem :: LPSPACC1:7

    

     Th7: h = (( multcomplexcpfunc 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 = (( multcomplexcpfunc 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 a1 = a as Element of COMPLEX by XCMPLX_0:def 2;

        reconsider k = (( multcomplexcpfunc A) . (a1,f)) as Element of ( PFuncs (A, COMPLEX ));

        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 = (( multcomplexcpfunc A) . (a,f)) by A2, A4, PARTFUN1: 5;

      end;

    end;

    registration

      let A;

      cluster ( addcpfunc A) -> commutative associative;

      coherence

      proof

        set o = ( addcpfunc A);

        hereby

          let F1,F2 be Element of ( PFuncs (A, COMPLEX ));

          

          thus (o . (F1,F2)) = (F2 + F1) by Def5

          .= (o . (F2,F1)) by Def5;

        end;

        let F1,F2,F3 be Element of ( PFuncs (A, COMPLEX ));

        

        thus (o . (F1,(o . (F2,F3)))) = (F1 + (o . (F2,F3))) by Def5

        .= (F1 + (F2 + F3)) by Def5

        .= ((F1 + F2) + F3) by RFUNCT_1: 8

        .= ((o . (F1,F2)) + F3) by Def5

        .= (o . ((o . (F1,F2)),F3)) by Def5;

      end;

    end

    registration

      let A;

      cluster ( multcpfunc A) -> commutative associative;

      coherence

      proof

        thus ( multcpfunc A) is commutative

        proof

          let f,g be Element of ( PFuncs (A, COMPLEX ));

          

           A1: ( dom (( multcpfunc A) . (g,f))) = (( dom g) /\ ( dom f)) by Th5;

          

           A2: ( dom (( multcpfunc A) . (f,g))) = (( dom f) /\ ( dom g)) by Th5;

          now

            let x be Element of A;

            assume

             A3: x in (( dom f) /\ ( dom g));

            

            hence ((( multcpfunc A) . (f,g)) . x) = ((g . x) * (f . x)) by A2, Th5

            .= ((( multcpfunc A) . (g,f)) . x) by A1, A3, Th5;

          end;

          hence thesis by A2, A1, PARTFUN1: 5;

        end;

        let f,g,h be Element of ( PFuncs (A, COMPLEX ));

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

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

        set j1 = (( multcpfunc A) . (f,j));

        set k1 = (( multcpfunc A) . (k,h));

        

         A4: ( dom k1) = (( dom k) /\ ( dom h)) by Th5;

        then

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

        

         A6: ( dom k1) = ((( dom f) /\ ( dom g)) /\ ( dom h)) by A4, Th5;

        

         A7: ( dom j1) = (( dom f) /\ ( dom j)) by Th5;

        then

         A8: ( dom j1) = (( dom f) /\ (( dom g) /\ ( dom h))) by Th5;

        

         A9: ( dom j1) c= ( dom j) by A7, XBOOLE_1: 17;

        now

          let x be Element of A;

          assume

           A10: x in ( dom j1);

          then

           A11: x in ( dom k1) by A8, A6, XBOOLE_1: 16;

          

          thus (j1 . x) = ((f . x) * (j . x)) by A10, Th5

          .= ((f . x) * ((g . x) * (h . x))) by A9, A10, Th5

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

          .= ((k . x) * (h . x)) by A5, A11, Th5

          .= (k1 . x) by A11, Th5;

        end;

        hence thesis by A8, A6, PARTFUN1: 5, XBOOLE_1: 16;

      end;

    end

    theorem :: LPSPACC1:8

    ( CPFuncUnit A) is_a_unity_wrt ( multcpfunc A)

    proof

      thus ( CPFuncUnit A) is_a_left_unity_wrt ( multcpfunc A)

      proof

        let f;

        set h = (( multcpfunc A) . (( CPFuncUnit A),f));

        ( dom h) = (( dom ( CPFuncUnit A)) /\ ( dom f)) by Th5;

        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) = ((( CPFuncUnit A) . x) * (f . x)) by A1, Th5;

          

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

          .= (f . x) by COMPLEX1:def 4;

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

        end;

        hence thesis by A1, PARTFUN1: 5;

      end;

      let f;

      set h = (( multcpfunc A) . (f,( CPFuncUnit A)));

      ( dom h) = (( dom ( CPFuncUnit A)) /\ ( dom f)) by Th5;

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

      then

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

      now

        let x be Element of A;

        assume x in ( dom f);

        then (h . x) = ((( CPFuncUnit A) . x) * (f . x)) by A2, Th5;

        

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

        .= (f . x) by COMPLEX1:def 4;

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

      end;

      hence thesis by A2, PARTFUN1: 5;

    end;

    theorem :: LPSPACC1:9

    

     Th9: ( CPFuncZero A) is_a_unity_wrt ( addcpfunc A)

    proof

      thus ( CPFuncZero A) is_a_left_unity_wrt ( addcpfunc A)

      proof

        let f;

        set h = (( addcpfunc A) . (( CPFuncZero A),f));

        ( dom h) = (( dom ( CPFuncZero A)) /\ ( dom f)) by Th4;

        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: (( CPFuncZero A) . x) = 0c by FUNCOP_1: 7;

          assume x in ( dom f);

          

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

          .= (f . x);

        end;

        hence thesis by A1, PARTFUN1: 5;

      end;

      let f;

      set h = (( addcpfunc A) . (f,( CPFuncZero A)));

      ( dom h) = (( dom ( CPFuncZero A)) /\ ( dom f)) by Th4;

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

      then

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

      now

        let x be Element of A;

        

         A4: (( CPFuncZero A) . x) = 0c by FUNCOP_1: 7;

        assume x in ( dom f);

        

        hence (h . x) = ( 0c + (f . x)) by A3, A4, Th4

        .= (f . x);

      end;

      hence thesis by A3, PARTFUN1: 5;

    end;

    reconsider R = ( - 1r ) as Element of COMPLEX by XCMPLX_0:def 2;

    theorem :: LPSPACC1:10

    

     Th10: (( addcpfunc A) . (f,(( multcomplexcpfunc A) . (( - 1r ),f)))) = (( CPFuncZero A) | ( dom f))

    proof

      reconsider g = (( multcomplexcpfunc A) . (R,f)) as Element of ( PFuncs (A, COMPLEX ));

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

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

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

      then

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

      

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

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

      now

        let x be Element of A;

        assume

         A3: x in ( dom f);

        then

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

        

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

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

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

        .= (( CPFuncZero A) . x) by FUNCOP_1: 7, COMPLEX1:def 4

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

      end;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: LPSPACC1:11

    

     Th11: (( multcomplexcpfunc A) . ( 1r ,f)) = f

    proof

      reconsider g = (( multcomplexcpfunc A) . ( 1r ,f)) as Element of ( PFuncs (A, COMPLEX ));

       A1:

      now

        let x be Element of A;

        assume x in ( dom f);

        

        hence (g . x) = ( 1r * (f . x)) by Th7

        .= (f . x) by COMPLEX1:def 4;

      end;

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

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: LPSPACC1:12

    

     Th12: (( multcomplexcpfunc A) . (a,(( multcomplexcpfunc A) . (b,f)))) = (( multcomplexcpfunc A) . ((a * b),f))

    proof

      reconsider a, b as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider c = (a * b) as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider g = (( multcomplexcpfunc A) . (b,f)) as Element of ( PFuncs (A, COMPLEX ));

      reconsider h = (( multcomplexcpfunc A) . (a,g)) as Element of ( PFuncs (A, COMPLEX ));

      reconsider k = (( multcomplexcpfunc A) . (c,f)) as Element of ( PFuncs (A, COMPLEX ));

      

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

      

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

       A3:

      now

        let x be Element of A;

        assume

         A4: x in ( dom h);

        

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

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

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

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

      end;

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

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

    end;

    theorem :: LPSPACC1:13

    

     Th13: (( addcpfunc A) . ((( multcomplexcpfunc A) . (a,f)),(( multcomplexcpfunc A) . (b,f)))) = (( multcomplexcpfunc A) . ((a + b),f))

    proof

      reconsider a, b as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider c = (a + b) as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider g = (( multcomplexcpfunc A) . (a,f)) as Element of ( PFuncs (A, COMPLEX ));

      reconsider h = (( multcomplexcpfunc A) . (b,f)) as Element of ( PFuncs (A, COMPLEX ));

      reconsider k = (( multcomplexcpfunc A) . (c,f)) as Element of ( PFuncs (A, COMPLEX ));

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

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

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

      then

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

       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, Th4

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

      end;

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

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    

     Lm1: (( addcpfunc A) . ((( multcomplexcpfunc A) . (a,f)),(( multcomplexcpfunc A) . (a,g)))) = (( multcomplexcpfunc A) . (a,(( addcpfunc A) . (f,g))))

    proof

      reconsider a as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider h = (( multcomplexcpfunc A) . (a,f)) as Element of ( PFuncs (A, COMPLEX ));

      reconsider i = (( multcomplexcpfunc A) . (a,g)) as Element of ( PFuncs (A, COMPLEX ));

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

      reconsider k = (( multcomplexcpfunc A) . (a,j)) as Element of ( PFuncs (A, COMPLEX ));

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

      

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

      

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

      

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

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

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

        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, Th4

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

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

        .= (a * (j . x)) by Def5

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

      end;

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

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

    end;

    theorem :: LPSPACC1:14

    (( multcpfunc A) . (f,(( addcpfunc A) . (g,h)))) = (( addcpfunc A) . ((( multcpfunc A) . (f,g)),(( multcpfunc A) . (f,h))))

    proof

      set i = (( multcpfunc A) . (f,h));

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

      set k = (( addcpfunc A) . (j,i));

      set l = (( addcpfunc A) . (g,h));

      set m = (( multcpfunc 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 Th5;

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

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

        then (l . x) = ((g + h) . x) & (k . x) = ((f . x) * ((g . x) + (h . x))) by A8, A10, Def5;

        then

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

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

        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 Th4, Th5;

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

    end;

    theorem :: LPSPACC1:15

    (( multcpfunc A) . ((( multcomplexcpfunc A) . (a,f)),g)) = (( multcomplexcpfunc A) . (a,(( multcpfunc A) . (f,g))))

    proof

      reconsider a as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider i = (( multcomplexcpfunc A) . (a,f)) as Element of ( PFuncs (A, COMPLEX ));

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

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

      reconsider l = (( multcomplexcpfunc A) . (a,j)) as Element of ( PFuncs (A, COMPLEX ));

      

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

      

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

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

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

      end;

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

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

    end;

    definition

      let A;

      :: LPSPACC1:def8

      func CLSp_PFunct A -> non empty CLSStruct equals CLSStruct (# ( PFuncs (A, COMPLEX )), ( CPFuncZero A), ( addcpfunc A), ( multcomplexcpfunc A) #);

      coherence ;

    end

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

    registration

      let A;

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

      coherence

      proof

        set IT = ( CLSp_PFunct A);

        thus IT is strict;

        thus (u + v) = (v + u) by BINOP_1:def 2;

        thus ((u + v) + w) = (u + (v + w)) by BINOP_1:def 3;

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

        proof

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

          

           A1: ( CPFuncZero A) is_a_unity_wrt ( addcpfunc A) by Th9;

          thus (u + ( 0. IT)) = u by A1, BINOP_1: 3;

        end;

        thus for a, u, v holds (a * (u + v)) = ((a * u) + (a * v))

        proof

          let a;

          reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;

          for u,v be VECTOR of ( CLSp_PFunct A) holds (a * (u + v)) = ((a * u) + (a * v))

          proof

            let u,v be VECTOR of ( CLSp_PFunct A);

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

            reconsider v9 = v as Element of ( PFuncs (A, COMPLEX ));

            (a1 * (u + v)) = (( multcomplexcpfunc A) . (a1,(( addcpfunc A) . (u9,v9))))

            .= (( addcpfunc A) . ((( multcomplexcpfunc A) . (a1,u9)),(( multcomplexcpfunc A) . (a1,v9)))) by Lm1

            .= ((a1 * u) + (a1 * v));

            hence thesis;

          end;

          hence thesis;

        end;

        thus for a,b be Complex, v holds ((a + b) * v) = ((a * v) + (b * v))

        proof

          let a,b be Complex, v be VECTOR of ( CLSp_PFunct A);

          reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def 2;

          reconsider v9 = v as Element of ( PFuncs (A, COMPLEX ));

          ((a1 + b1) * v) = (( multcomplexcpfunc A) . ((a1 + b1),v9))

          .= (( addcpfunc A) . ((( multcomplexcpfunc A) . (a1,v9)),(( multcomplexcpfunc A) . (b1,v9)))) by Th13

          .= ((a1 * v) + (b1 * v));

          hence thesis;

        end;

        thus for a,b be Complex, v holds ((a * b) * v) = (a * (b * v))

        proof

          let a,b be Complex, v be VECTOR of ( CLSp_PFunct A);

          reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def 2;

          reconsider v9 = v as Element of ( PFuncs (A, COMPLEX ));

          ((a1 * b1) * v) = (( multcomplexcpfunc A) . ((a1 * b1),v9))

          .= (( multcomplexcpfunc A) . (a1,(( multcomplexcpfunc A) . (b1,v9)))) by Th12

          .= (a1 * (b1 * v));

          hence thesis;

        end;

        let v;

        reconsider v9 = v as Element of ( PFuncs (A, COMPLEX ));

        ( 1r * v) = (( multcomplexcpfunc A) . ( 1r ,v9))

        .= v by Th11;

        hence ( 1r * v) = v;

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

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

    registration

      let X;

      let f be PartFunc of X, COMPLEX ;

      cluster ( abs f) -> nonnegative;

      coherence

      proof

        now

          let x be object;

          assume x in ( dom ( abs f));

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

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

        end;

        hence thesis by MESFUNC6: 52;

      end;

    end

    theorem :: LPSPACC1:16

    

     Th16: for f be PartFunc of X, COMPLEX st ( dom f) in S & for x st x in ( dom f) holds 0 = (f . x) holds f is_integrable_on M & ( Integral (M,f)) = 0

    proof

      let f be PartFunc of X, COMPLEX ;

      assume ( dom f) in S;

      then

      reconsider E = ( dom f) as Element of S;

      assume

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

      

       A2: for x st x in ( dom f) holds (( Re f) . x) = 0 & (( Im f) . x) = 0

      proof

        let x such that

         A3: x in ( dom f);

        

         A4: x in ( dom ( Re f)) & x in ( dom ( Im f)) by A3, COMSEQ_3:def 3, COMSEQ_3:def 4;

        

         A5: (( Re f) . x) = ( Re (f . x)) by COMSEQ_3:def 3, A4

        .= 0 by A3, A1, COMPLEX1: 4;

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

        .= 0 by A3, A1, COMPLEX1: 4;

        hence thesis by A5;

      end;

      

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

      

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

      set f1 = ( Re f);

      

       A8: E = ( dom f1) & for x st x in ( dom f1) holds 0 = (f1 . x) by A2, A6;

      

       A9: ( R_EAL f1) is_integrable_on M & ( Integral (M,( R_EAL f1))) = 0 by LPSPACE1: 22, A8;

      

       A10: ( Re f) is_integrable_on M & ( Integral (M,( Re f))) = 0 by A9;

      set f2 = ( Im f);

      

       A11: E = ( dom f2) & for x st x in ( dom f2) holds 0 = (f2 . x) by A2, A7;

      

       A12: ( R_EAL f2) is_integrable_on M & ( Integral (M,( R_EAL f2))) = 0 by LPSPACE1: 22, A11;

      

       A13: ( Im f) is_integrable_on M & ( Integral (M,( Im f))) = 0 by A12;

      f is_integrable_on M by A10, A13, MESFUN6C:def 2;

      then ex RF,IF be Real st RF = ( Integral (M,( Re f))) & IF = ( Integral (M,( Im f))) & ( Integral (M,f)) = (RF + (IF * <i> )) by MESFUN6C:def 3;

      hence thesis by A10, A13, MESFUN6C:def 2;

    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 X = ( dom f) & for x st x in ( dom f) holds 0 = (f . x);

      hence thesis by A1, Th16;

    end;

    definition

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

      :: LPSPACC1:def9

      func L1_CFunctions M -> non empty Subset of ( CLSp_PFunct X) equals { f where f be PartFunc of X, COMPLEX : 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: 7;

        set g = (X --> 0c );

        set I = { f where f be PartFunc of X, COMPLEX : ex ND be Element of S st (M . ND) = 0 & ( dom f) = (ND ` ) & f is_integrable_on M };

        

         A1: I c= ( PFuncs (X, COMPLEX ))

        proof

          let x be object;

          assume x in I;

          then ex f be PartFunc of X, COMPLEX 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 ) in ( L1_CFunctions M)

    proof

      set g = (X --> 0c );

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

      

       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;

      hence thesis by MEASURE1: 37, MEASURE1:def 7;

    end;

    theorem :: LPSPACC1:17

    

     Th17: f in ( L1_CFunctions M) & g in ( L1_CFunctions M) implies (f + g) in ( L1_CFunctions M)

    proof

      set W = ( L1_CFunctions M);

      assume that

       A1: f in W and

       A2: g in W;

      ex f1 be PartFunc of X, COMPLEX 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, COMPLEX 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, MESFUN6C: 33;

      hence thesis by A9;

    end;

    theorem :: LPSPACC1:18

    

     Th18: f in ( L1_CFunctions M) implies (a (#) f) in ( L1_CFunctions M)

    proof

      set W = ( L1_CFunctions M);

      assume f in W;

      then ex f1 be PartFunc of X, COMPLEX 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, MESFUN6C: 40, VALUED_1:def 5;

      hence thesis by A1;

    end;

    

     Lm5: ( L1_CFunctions M) is add-closed & ( L1_CFunctions M) is multi-closed

    proof

      set W = ( L1_CFunctions M);

      now

        let v,u be Element of ( CLSp_PFunct X) such that

         A1: v in W and

         A2: u in W;

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

        consider v1 be PartFunc of X, COMPLEX 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, COMPLEX 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, Th4;

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

        hence (v + u) in ( L1_CFunctions M) by A1, A2, A3, A4, Th17;

      end;

      hence ( L1_CFunctions M) is add-closed;

      now

        let a be Complex, u be VECTOR of ( CLSp_PFunct X) such that

         A5: u in W;

        reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;

        consider u1 be PartFunc of X, COMPLEX 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 = (a1 * u) as Element of ( PFuncs (X, COMPLEX ));

        

         A7: (a1 * u) = (( multcomplexcpfunc X) . (a,u));

        then

         A8: ( dom h) = ( dom u1) by A6, Th7;

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

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

        hence (a * u) in ( L1_CFunctions M) by A5, A6, Th18;

      end;

      hence thesis;

    end;

    registration

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

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

      :: LPSPACC1:def10

      func CLSp_L1Funct M -> non empty CLSStruct equals CLSStruct (# ( L1_CFunctions M), ( In (( 0. ( CLSp_PFunct X)),( L1_CFunctions M))), ( add| (( L1_CFunctions M),( CLSp_PFunct X))), ( Mult_ ( L1_CFunctions M)) #);

      coherence ;

    end

    registration

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

      cluster ( CLSp_L1Funct M) -> strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        ( 0. ( CLSp_PFunct X)) in ( L1_CFunctions M) by Lm3;

        hence thesis by Th3;

      end;

    end

    begin

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

    theorem :: LPSPACC1:19

    

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

    proof

      reconsider v2 = v, u2 = u as VECTOR of ( CLSp_PFunct X) by TARSKI:def 3;

      reconsider h = (v2 + u2) as Element of ( PFuncs (X, COMPLEX ));

      reconsider v3 = v2, u3 = u2 as Element of ( PFuncs (X, COMPLEX ));

      

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

      assume

       A2: f = v & g = u;

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

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

      hence thesis by ZFMISC_1: 87, FUNCT_1: 49;

    end;

    theorem :: LPSPACC1:20

    

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

    proof

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

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

      assume

       A1: f = u;

      

       A2: (a * u2) = (( multcomplexcpfunc X) . (a,u2));

      

       A3: ( dom h) = ( dom f) by A1, A2, Th7;

      

       A4: for x be object st x in ( dom h) holds (h . x) = (a * (f . x)) by A1, A2, A3, Th7;

      

       A5: h = (a (#) f) by A3, A4, VALUED_1:def 5;

      reconsider a as Element of COMPLEX by XCMPLX_0:def 2;

       [a, u] in [: COMPLEX , ( L1_CFunctions M):];

      hence thesis by A5, FUNCT_1: 49;

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

      :: LPSPACC1:def11

      pred f a.e.cpfunc= g,M means

      : Def11: ex E be Element of S st (M . E) = 0 & (f | (E ` )) = (g | (E ` ));

    end

    theorem :: LPSPACC1:21

    

     Th21: f = u implies (u + (( - 1r ) * u)) = ((X --> 0c ) | ( dom f)) & ex v,g be PartFunc of X, COMPLEX st v in ( L1_CFunctions M) & g in ( L1_CFunctions M) & v = (u + (( - 1r ) * u)) & g = (X --> 0c ) & v a.e.cpfunc= (g,M)

    proof

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

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

      set g = (X --> 0c );

      (u + (( - 1r ) * u)) in ( L1_CFunctions M);

      then

      consider v be PartFunc of X, COMPLEX such that

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

      assume

       A2: f = u;

      reconsider u9 = u2 as Element of ( PFuncs (X, COMPLEX ));

      

       A3: h = (( addcpfunc X) . (u2,(( multcomplexcpfunc X) . (( - 1r ),u2))))

      .= (( CPFuncZero X) | ( dom f)) by A2, Th10;

      u in ( L1_CFunctions M);

      then ex uu1 be PartFunc of X, COMPLEX 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;

       [R, u] in [: COMPLEX , ( L1_CFunctions M):];

      then

       A6: (( - 1r ) * u2) = (( - 1r ) * u) by FUNCT_1: 49;

      hence (u + (( - 1r ) * u)) = ((X --> 0 ) | ( dom f)) by A3, ZFMISC_1: 87, FUNCT_1: 49;

      (v | (ND ` )) = ((g | (ND ` )) | (ND ` )) by A3, A6, A1, A5, ZFMISC_1: 87, FUNCT_1: 49;

      then

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

      g in ( L1_CFunctions M) by Lm3;

      hence thesis by A1, A4, A7, Def11;

    end;

    theorem :: LPSPACC1:22

    

     Th22: f a.e.cpfunc= (f,M)

    proof

       {} is Element of S by MEASURE1: 7;

      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 :: LPSPACC1:23

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

    theorem :: LPSPACC1:24

    

     Th24: f a.e.cpfunc= (g,M) & g a.e.cpfunc= (h,M) implies f a.e.cpfunc= (h,M)

    proof

      assume that

       A1: f a.e.cpfunc= (g,M) and

       A2: g a.e.cpfunc= (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 :: LPSPACC1:25

    

     Th25: f a.e.cpfunc= (f1,M) & g a.e.cpfunc= (g1,M) implies (f + g) a.e.cpfunc= ((f1 + g1),M)

    proof

      assume that

       A1: f a.e.cpfunc= (f1,M) and

       A2: g a.e.cpfunc= (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 :: LPSPACC1:26

    

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

    proof

      assume f a.e.cpfunc= (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;

      :: LPSPACC1:def12

      func AlmostZeroCFunctions M -> non empty Subset of ( CLSp_L1Funct M) equals { f where f be PartFunc of X, COMPLEX : f in ( L1_CFunctions M) & f a.e.cpfunc= ((X --> 0c ),M) };

      coherence

      proof

         A1:

        now

          let x be object;

          assume x in { f where f be PartFunc of X, COMPLEX : f in ( L1_CFunctions M) & f a.e.cpfunc= ((X --> 0c ),M) };

          then ex f be PartFunc of X, COMPLEX st x = f & f in ( L1_CFunctions M) & f a.e.cpfunc= ((X --> 0c ),M);

          hence x in the carrier of ( CLSp_L1Funct M);

        end;

        (X --> 0c ) a.e.cpfunc= ((X --> 0c ),M) & (X --> 0 ) in ( L1_CFunctions M) by Lm3, Th22;

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

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: LPSPACC1:27

    

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

    proof

      set g1 = (X --> 0c );

      set g2 = (X --> 0c );

       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 --> 0c ) . 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 --> 0c ));

        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 --> 0c ) . x);

      end;

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

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

      hence thesis by A1, PARTFUN1: 5;

    end;

    

     Lm6: ( AlmostZeroCFunctions M) is add-closed & ( AlmostZeroCFunctions M) is multi-closed

    proof

      set Z = ( AlmostZeroCFunctions M);

      set V = ( CLSp_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, COMPLEX such that

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

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

        consider u1 be PartFunc of X, COMPLEX such that

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

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

        

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

        ((X --> 0c ) + (X --> 0c )) = (X --> 0c ) by Th27;

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

        hence (v + u) in Z by A7;

      end;

      hence Z is add-closed;

      now

        let a be Complex, u be VECTOR of V;

        reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;

        assume u in Z;

        then

        consider u1 be PartFunc of X, COMPLEX such that

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

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

        

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

        (a1 (#) (X --> 0 )) = (X --> 0 ) by Th27;

        then (a1 (#) u1) a.e.cpfunc= ((X --> 0c ),M) by A9, Th26;

        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 ( AlmostZeroCFunctions M) -> add-closed multi-closed;

      coherence by Lm6;

    end

    theorem :: LPSPACC1:28

    ( 0. ( CLSp_L1Funct M)) = (X --> 0c ) & ( 0. ( CLSp_L1Funct M)) in ( AlmostZeroCFunctions M)

    proof

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

      (X --> 0c ) a.e.cpfunc= ((X --> 0c ),M) & ( 0. ( CLSp_L1Funct M)) = ( 0. ( CLSp_PFunct X)) by Lm3, Th22, 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;

      :: LPSPACC1:def13

      func CLSp_AlmostZeroFunct M -> non empty CLSStruct equals CLSStruct (# ( AlmostZeroCFunctions M), ( In (( 0. ( CLSp_L1Funct M)),( AlmostZeroCFunctions M))), ( add| (( AlmostZeroCFunctions M),( CLSp_L1Funct M))), ( Mult_ ( AlmostZeroCFunctions M)) #);

      coherence ;

    end

    registration

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

      cluster ( CLSp_L1Funct M) -> strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence ;

    end

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

    theorem :: LPSPACC1:29

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

    proof

      assume

       A1: f = v & g = u;

      reconsider v2 = v, u2 = u as VECTOR of ( CLSp_L1Funct M) by TARSKI:def 3;

      

      thus (v + u) = (v2 + u2) by ZFMISC_1: 87, FUNCT_1: 49

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

    end;

    definition

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

      :: LPSPACC1:def14

      func a.e-Ceq-class (f,M) -> Subset of ( L1_CFunctions M) equals { g where g be PartFunc of X, COMPLEX : g in ( L1_CFunctions M) & f in ( L1_CFunctions M) & f a.e.cpfunc= (g,M) };

      correctness

      proof

        now

          let x be object;

          assume x in { g where g be PartFunc of X, COMPLEX : g in ( L1_CFunctions M) & f in ( L1_CFunctions M) & f a.e.cpfunc= (g,M) };

          then ex g be PartFunc of X, COMPLEX st x = g & g in ( L1_CFunctions M) & f in ( L1_CFunctions M) & f a.e.cpfunc= (g,M);

          hence x in ( L1_CFunctions M);

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: LPSPACC1:30

    

     Th30: f in ( L1_CFunctions M) & g in ( L1_CFunctions M) implies (g a.e.cpfunc= (f,M) iff g in ( a.e-Ceq-class (f,M)))

    proof

      assume

       A1: f in ( L1_CFunctions M) & g in ( L1_CFunctions M);

      hereby

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

        then f a.e.cpfunc= (g,M);

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

      end;

      assume g in ( a.e-Ceq-class (f,M));

      then ex r be PartFunc of X, COMPLEX st g = r & r in ( L1_CFunctions M) & f in ( L1_CFunctions M) & f a.e.cpfunc= (r,M);

      hence g a.e.cpfunc= (f,M);

    end;

    theorem :: LPSPACC1:31

    

     Th31: f in ( L1_CFunctions M) implies f in ( a.e-Ceq-class (f,M))

    proof

      assume

       A1: f in ( L1_CFunctions M);

      f a.e.cpfunc= (f,M) by Th22;

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

    end;

    theorem :: LPSPACC1:32

    

     Th32: f in ( L1_CFunctions M) & g in ( L1_CFunctions M) implies (( a.e-Ceq-class (f,M)) = ( a.e-Ceq-class (g,M)) iff f a.e.cpfunc= (g,M))

    proof

      assume that

       A1: f in ( L1_CFunctions M) and

       A2: g in ( L1_CFunctions M);

      hereby

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

        then f in { r where r be PartFunc of X, COMPLEX : r in ( L1_CFunctions M) & g in ( L1_CFunctions M) & g a.e.cpfunc= (r,M) } by A1, Th31;

        then ex r be PartFunc of X, COMPLEX st f = r & r in ( L1_CFunctions M) & g in ( L1_CFunctions M) & g a.e.cpfunc= (r,M);

        hence f a.e.cpfunc= (g,M);

      end;

      assume

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

      now

        let x be object;

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

        then

        consider r be PartFunc of X, COMPLEX such that

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

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

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

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

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

      end;

      then

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

      now

        let x be object;

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

        then

        consider r be PartFunc of X, COMPLEX such that

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

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

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

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

      end;

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

      hence thesis by A6, XBOOLE_0:def 10;

    end;

    theorem :: LPSPACC1:33

    f in ( L1_CFunctions M) & g in ( L1_CFunctions M) implies (( a.e-Ceq-class (f,M)) = ( a.e-Ceq-class (g,M)) iff g in ( a.e-Ceq-class (f,M)))

    proof

      assume

       A1: f in ( L1_CFunctions M) & g in ( L1_CFunctions M);

      then g a.e.cpfunc= (f,M) iff g in ( a.e-Ceq-class (f,M)) by Th30;

      hence thesis by A1, Th32;

    end;

    theorem :: LPSPACC1:34

    

     Th34: f in ( L1_CFunctions M) & f1 in ( L1_CFunctions M) & g in ( L1_CFunctions M) & g1 in ( L1_CFunctions M) & ( a.e-Ceq-class (f,M)) = ( a.e-Ceq-class (f1,M)) & ( a.e-Ceq-class (g,M)) = ( a.e-Ceq-class (g1,M)) implies ( a.e-Ceq-class ((f + g),M)) = ( a.e-Ceq-class ((f1 + g1),M))

    proof

      assume that

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

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

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

      then

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

      (f + g) in ( L1_CFunctions M) & (f1 + g1) in ( L1_CFunctions M) by A1, Th17;

      hence thesis by A3, Th32;

    end;

    theorem :: LPSPACC1:35

    

     Th35: f in ( L1_CFunctions M) & g in ( L1_CFunctions M) & ( a.e-Ceq-class (f,M)) = ( a.e-Ceq-class (g,M)) implies ( a.e-Ceq-class ((a (#) f),M)) = ( a.e-Ceq-class ((a (#) g),M))

    proof

      assume that

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

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

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

      then

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

      (a (#) f) in ( L1_CFunctions M) & (a (#) g) in ( L1_CFunctions M) by A1, Th18;

      hence thesis by A3, Th32;

    end;

    definition

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

      :: LPSPACC1:def15

      func CCosetSet M -> non empty Subset-Family of ( L1_CFunctions M) equals { ( a.e-Ceq-class (f,M)) where f be PartFunc of X, COMPLEX : f in ( L1_CFunctions M) };

      correctness

      proof

        set C = { ( a.e-Ceq-class (f,M)) where f be PartFunc of X, COMPLEX : f in ( L1_CFunctions M) };

        

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

        proof

          let x be object;

          assume x in C;

          then ex f be PartFunc of X, COMPLEX st ( a.e-Ceq-class (f,M)) = x & f in ( L1_CFunctions M);

          hence thesis;

        end;

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

        then ( a.e-Ceq-class ((X --> 0c ),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;

      :: LPSPACC1:def16

      func addCCoset M -> BinOp of ( CCosetSet M) means

      : Def16: for A,B be Element of ( CCosetSet M), a,b be PartFunc of X, COMPLEX st a in A & b in B holds (it . (A,B)) = ( a.e-Ceq-class ((a + b),M));

      existence

      proof

        defpred P[ set, set, set] means for a,b be PartFunc of X, COMPLEX st a in $1 & b in $2 holds $3 = ( a.e-Ceq-class ((a + b),M));

        set C = ( CCosetSet M);

         A1:

        now

          let A,B be Element of C;

          A in C;

          then

          consider a be PartFunc of X, COMPLEX such that

           A2: A = ( a.e-Ceq-class (a,M)) and

           A3: a in ( L1_CFunctions M);

          B in C;

          then

          consider b be PartFunc of X, COMPLEX such that

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

           A5: b in ( L1_CFunctions M);

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

          

           A6: (a + b) in ( L1_CFunctions M) by A3, A5, Th17;

          then z in C;

          then

          reconsider z as Element of C;

          take z;

          now

            let a1,b1 be PartFunc of X, COMPLEX ;

            assume

             A7: a1 in A & b1 in B;

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

            then

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

            (a1 + b1) in ( L1_CFunctions M) by A7, Th17;

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

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

        assume a in A & b in B;

        hence thesis by A9;

      end;

      uniqueness

      proof

        set C = ( CCosetSet M);

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

         A10: for A,B be Element of ( CCosetSet M), a,b be PartFunc of X, COMPLEX st a in A & b in B holds (f1 . (A,B)) = ( a.e-Ceq-class ((a + b),M)) and

         A11: for A,B be Element of ( CCosetSet M), a,b be PartFunc of X, COMPLEX st a in A & b in B holds (f2 . (A,B)) = ( a.e-Ceq-class ((a + b),M));

        now

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

          A in C;

          then

          consider a1 be PartFunc of X, COMPLEX such that

           A12: A = ( a.e-Ceq-class (a1,M)) & a1 in ( L1_CFunctions M);

          B in C;

          then

          consider b1 be PartFunc of X, COMPLEX such that

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

          

           A14: b1 in B by A13, Th31;

          

           A15: a1 in A by A12, Th31;

          then (f1 . (A,B)) = ( a.e-Ceq-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;

      :: LPSPACC1:def17

      func zeroCCoset M -> Element of ( CCosetSet M) equals ( a.e-Ceq-class ((X --> 0c ),M));

      correctness

      proof

        (X --> 0c ) in ( L1_CFunctions M) by Lm3;

        then ( a.e-Ceq-class ((X --> 0c ),M)) in ( CCosetSet M);

        hence thesis;

      end;

    end

    definition

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

      :: LPSPACC1:def18

      func lmultCCoset M -> Function of [: COMPLEX , ( CCosetSet M):], ( CCosetSet M) means

      : Def18: for z be Complex, A be Element of ( CCosetSet M), f be PartFunc of X, COMPLEX st f in A holds (it . (z,A)) = ( a.e-Ceq-class ((z (#) f),M));

      existence

      proof

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

        set C = ( CCosetSet M);

         A1:

        now

          let z be Element of COMPLEX , A be Element of C;

          A in C;

          then

          consider a be PartFunc of X, COMPLEX such that

           A2: A = ( a.e-Ceq-class (a,M)) and

           A3: a in ( L1_CFunctions M);

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

          

           A4: (z (#) a) in ( L1_CFunctions M) by A3, Th18;

          then c in C;

          then

          reconsider c as Element of C;

          take c;

          now

            let a1 be PartFunc of X, COMPLEX ;

            assume

             A5: a1 in A;

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

            then

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

            (z (#) a1) in ( L1_CFunctions M) by A5, Th18;

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

          end;

          hence P[z, A, c];

        end;

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

         A7: for z be Element of COMPLEX , A be Element of C holds P[z, A, (f . (z,A))] from BINOP_1:sch 3( A1);

        take f;

        let z be Complex, A be Element of C, a be PartFunc of X, COMPLEX ;

        z in COMPLEX by XCMPLX_0:def 2;

        hence thesis by A7;

      end;

      uniqueness

      proof

        set C = ( CCosetSet M);

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

         A8: for z be Complex, A be Element of ( CCosetSet M), a be PartFunc of X, COMPLEX st a in A holds (f1 . (z,A)) = ( a.e-Ceq-class ((z (#) a),M)) and

         A9: for z be Complex, A be Element of ( CCosetSet M), a be PartFunc of X, COMPLEX st a in A holds (f2 . (z,A)) = ( a.e-Ceq-class ((z (#) a),M));

        now

          let z be Element of COMPLEX , A be Element of ( CCosetSet M);

          A in C;

          then

          consider a1 be PartFunc of X, COMPLEX such that

           A10: A = ( a.e-Ceq-class (a1,M)) & a1 in ( L1_CFunctions M);

          

          thus (f1 . (z,A)) = ( a.e-Ceq-class ((z (#) a1),M)) by A8, A10, Th31

          .= (f2 . (z,A)) by A9, A10, Th31;

        end;

        hence thesis;

      end;

    end

    definition

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

      :: LPSPACC1:def19

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

      : Def19: the carrier of it = ( CCosetSet M) & the addF of it = ( addCCoset M) & ( 0. it ) = ( zeroCCoset M) & the Mult of it = ( lmultCCoset M);

      existence

      proof

        set C = ( CCosetSet M), aC = ( addCCoset M), zC = ( zeroCCoset M), lC = ( lmultCCoset M), A = CLSStruct (# 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, COMPLEX such that

           A2: A1 = ( a.e-Ceq-class (a,M)) & a in ( L1_CFunctions M);

          A2 in C;

          then

          consider b be PartFunc of X, COMPLEX such that

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

          

           A4: b in A2 by A3, Th31;

          

           A5: a in A1 by A2, Th31;

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

          hence thesis by A5, A4, Def16;

        end;

        

         A6: A is right_zeroed

        proof

          set z = (X --> 0c );

          

           A7: z in ( L1_CFunctions M) by Lm3;

          

           A8: z in ( 0. A) by A7, Th31;

          let A1 be Element of A;

          A1 in C;

          then

          consider a be PartFunc of X, COMPLEX such that

           A9: A1 = ( a.e-Ceq-class (a,M)) and

           A10: a in ( L1_CFunctions M);

          reconsider a1 = a as VECTOR of ( CLSp_L1Funct M) by A10;

          reconsider a1 = a, z1 = z as VECTOR of ( CLSp_L1Funct M) by A10, A7;

          

           A11: (a + z) = (a1 + z1) by Th19

          .= (a1 + ( 0. ( CLSp_L1Funct M)))

          .= a by RLVECT_1:def 4;

          a in A1 by A9, A10, Th31;

          hence thesis by A9, A8, A11, Def16;

        end;

         A12:

        now

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

          reconsider x1 = x, y1 = y as Element of COMPLEX by XCMPLX_0:def 2;

          A1 in C;

          then

          consider a be PartFunc of X, COMPLEX such that

           A13: A1 = ( a.e-Ceq-class (a,M)) and

           A14: a in ( L1_CFunctions M);

          

           A15: a in A1 by A13, A14, Th31;

          (lC . (x1,A1)) = ( a.e-Ceq-class ((x (#) a),M)) by A13, A14, Th31, Def18;

          then

           A16: (x (#) a) in (x * A1) by A14, Th18, Th31;

          A2 in C;

          then

          consider b be PartFunc of X, COMPLEX such that

           A17: A2 = ( a.e-Ceq-class (b,M)) and

           A18: b in ( L1_CFunctions M);

          reconsider a1 = a, b1 = b as VECTOR of ( CLSp_L1Funct M) by A14, A18;

          

           A19: (x (#) a) = (x1 * a1) by Th20;

          

           A20: b in A2 by A17, A18, Th31;

          (lC . (x1,A2)) = ( a.e-Ceq-class ((x (#) b),M)) by A17, A18, Th31, Def18;

          then

           A21: (x (#) b) in (x1 * A2) by A18, Th18, Th31;

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

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

          then

           A22: (x (#) (a + b)) = ((x * a1) + (x * b1)) by CLVECT_1:def 2;

          

           A23: (x (#) b) = (x1 * b1) by Th20;

          (aC . (A1,A2)) = ( a.e-Ceq-class ((a + b),M)) by A15, A20, Def16;

          then

           A24: (a + b) in (A1 + A2) by A14, A18, Th17, Th31;

          (x1 * (A1 + A2)) = (lC . (x1,(A1 + A2)))

          .= ( a.e-Ceq-class ((x (#) (a + b)),M)) by A24, Def18

          .= ( a.e-Ceq-class (((x (#) a) + (x (#) b)),M)) by A19, A22, A23, Th19;

          hence (x * (A1 + A2)) = ((x * A1) + (x * A2)) by A16, A21, Def16;

          

           A25: (y (#) a) = (y1 * a1) by Th20;

          (lC . (y1,A1)) = ( a.e-Ceq-class ((y (#) a),M)) by A13, A14, Th31, Def18;

          then

           A26: (y (#) a) in (y1 * A1) by A14, Th18, Th31;

          

           A27: ((x + y) (#) a) = ((x1 + y1) * a1) by Th20

          .= ((x * a1) + (y * a1)) by CLVECT_1:def 3

          .= ((x (#) a) + (y (#) a)) by A25, A19, Th19;

          ((x1 + y1) * A1) = (lC . ((x1 + y1),A1))

          .= ( a.e-Ceq-class (((x (#) a) + (y (#) a)),M)) by A27, A13, A14, Th31, Def18;

          hence ((x + y) * A1) = ((x * A1) + (y * A1)) by A16, A26, Def16;

          

           A28: (x1 (#) (y1 (#) a)) = (x1 * (y1 * a1)) by A25, Th20

          .= ((x1 * y1) * a1) by CLVECT_1:def 4

          .= ((x1 * y1) (#) a) by Th20;

          ((x1 * y1) * A1) = (lC . ((x1 * y1),A1))

          .= ( a.e-Ceq-class ((x1 (#) (y1 (#) a)),M)) by A28, A13, A14, Th31, Def18

          .= (lC . (x1,(y1 * A1))) by A26, Def18

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

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

          

           A29: ( 1r (#) a) = ( 1r * a1) by Th20

          .= a by CLVECT_1:def 5;

          

          thus ( 1r * A1) = (lC . ( 1r ,A1))

          .= A1 by A13, A29, A14, Th31, Def18;

        end;

        

         A30: A is right_complementable

        proof

          let A1 be Element of A;

          A1 in C;

          then

          consider a be PartFunc of X, COMPLEX such that

           A31: A1 = ( a.e-Ceq-class (a,M)) and

           A32: a in ( L1_CFunctions M);

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

          

           A33: (( - 1r ) (#) a) in ( L1_CFunctions M) by A32, Th18;

          then A2 in C;

          then

          reconsider A2 as Element of A;

          

           A34: a in A1 & (( - 1r ) (#) a) in A2 by A31, A32, Th18, Th31;

          reconsider a1 = a as VECTOR of ( CLSp_L1Funct M) by A32;

          take A2;

          consider v,g be PartFunc of X, COMPLEX such that v in ( L1_CFunctions M) and g in ( L1_CFunctions M) and

           A35: v = (a1 + (( - 1r ) * a1)) and

           A36: g = (X --> 0c ) and

           A37: v a.e.cpfunc= (g,M) by Th21;

          

           A38: (X --> 0c ) in ( L1_CFunctions M) by Lm3;

          

           A39: (a + (( - 1r ) (#) a)) in ( L1_CFunctions M) by A32, A33, Th17;

          (( - 1r ) (#) a) = (( - 1r ) * a1) by Th20;

          then (a + (( - 1r ) (#) a)) a.e.cpfunc= (g,M) by A35, A37, Th19;

          then ( 0. A) = ( a.e-Ceq-class ((a + (( - 1r ) (#) a)),M)) by A36, A39, A38, Th32;

          hence thesis by A34, Def16;

        end;

        A is add-associative

        proof

          let A1,A2,A3 be Element of A;

          A1 in C;

          then

          consider a be PartFunc of X, COMPLEX such that

           A40: A1 = ( a.e-Ceq-class (a,M)) and

           A41: a in ( L1_CFunctions M);

          A2 in C;

          then

          consider b be PartFunc of X, COMPLEX such that

           A42: A2 = ( a.e-Ceq-class (b,M)) and

           A43: b in ( L1_CFunctions M);

          A3 in C;

          then

          consider c be PartFunc of X, COMPLEX such that

           A44: A3 = ( a.e-Ceq-class (c,M)) and

           A45: c in ( L1_CFunctions M);

          

           A46: c in A3 by A44, A45, Th31;

          

           A47: b in A2 by A42, A43, Th31;

          then (aC . (A2,A3)) = ( a.e-Ceq-class ((b + c),M)) by A46, Def16;

          then

           A48: (b + c) in (A2 + A3) by A43, A45, Th17, Th31;

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

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

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

          then

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

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

          then

           A50: (a + (b + c)) = ((a + b) + c) by A49, Th19;

          

           A51: a in A1 by A40, A41, Th31;

          then (aC . (A1,A2)) = ( a.e-Ceq-class ((a + b),M)) by A47, Def16;

          then (a + b) in (A1 + A2) by A41, A43, Th17, Th31;

          then ((A1 + A2) + A3) = ( a.e-Ceq-class ((a + (b + c)),M)) by A46, A50, Def16;

          hence thesis by A51, A48, Def16;

        end;

        then

        reconsider A as strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct by A1, A6, A30, A12, CLVECT_1:def 2, CLVECT_1:def 3, CLVECT_1:def 4, CLVECT_1:def 5;

        take A;

        thus thesis;

      end;

      uniqueness ;

    end

    begin

    theorem :: LPSPACC1:36

    

     Th36: f in ( L1_CFunctions M) & g in ( L1_CFunctions M) & f a.e.cpfunc= (g,M) implies ( Integral (M,f)) = ( Integral (M,g))

    proof

      assume that

       A1: f in ( L1_CFunctions M) and

       A2: g in ( L1_CFunctions M) and

       A3: f a.e.cpfunc= (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, COMPLEX 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;

      consider E1 be Element of S such that

       A10: E1 = ( dom f) and f is E1 -measurable by A6, MESFUN7C: 35;

      

       A11: ex g1 be PartFunc of X, COMPLEX 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: (M . (EQ \/ NDg)) = 0 by A12, A4, Lm4;

      consider E2 be Element of S such that

       A15: E2 = ( dom g) and g is E2 -measurable by A11, MESFUN7C: 35;

      

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

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

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

      

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

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

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

      

       A18: ((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 A18, FUNCT_1: 51;

      

      hence ( Integral (M,f)) = ( Integral (M,(g | ((NDg ` ) \ (EQ \/ NDf))))) by A6, A8, A10, A17, A16, A14, MESFUN6C: 22

      .= ( Integral (M,g)) by A11, A13, A15, A9, MESFUN6C: 22;

    end;

    theorem :: LPSPACC1:37

    

     Th37: f is_integrable_on M implies ( Integral (M,f)) in COMPLEX & ( Integral (M, |.f.|)) in REAL & |.f.| is_integrable_on M

    proof

      assume

       A1: f is_integrable_on M;

      reconsider AF = |.f.| as PartFunc of X, REAL ;

      AF is_integrable_on M by A1, MESFUN7C: 35;

      hence thesis by LPSPACE1: 44, XCMPLX_0:def 2;

    end;

    theorem :: LPSPACC1:38

    

     Th38: f in ( L1_CFunctions M) & g in ( L1_CFunctions M) & f a.e.cpfunc= (g,M) implies |.f.| a.e.= ( |.g.|,M) & ( Integral (M, |.f.|)) = ( Integral (M, |.g.|))

    proof

      assume that

       A1: f in ( L1_CFunctions M) and

       A2: g in ( L1_CFunctions M) and

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

      reconsider AF = |.f.|, AG = |.g.| as PartFunc of X, REAL ;

      

       A4: ex f1 be PartFunc of X, COMPLEX 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: AF is_integrable_on M by A4, Th37;

      consider EQ be Element of S such that

       A8: (M . EQ) = 0 and

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

      

       A10: (AF | (EQ ` )) = ( abs (g | (EQ ` ))) by A9, CFUNCT_1: 54

      .= (AG | (EQ ` )) by CFUNCT_1: 54;

      

       A11: ex g1 be PartFunc of X, COMPLEX 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: AG is_integrable_on M by A11, Th37;

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

      then

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

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

      then AF in ( L1_Functions M) by A5, A7;

      hence thesis by A15, A8, A10, LPSPACE1:def 10, LPSPACE1: 43;

    end;

    theorem :: LPSPACC1:39

    

     Th39: (ex x be VECTOR of ( Pre-L-CSpace M) st f in x & g in x) implies f a.e.cpfunc= (g,M) & f in ( L1_CFunctions M) & g in ( L1_CFunctions M)

    proof

      given x be VECTOR of ( Pre-L-CSpace M) such that

       A1: f in x and

       A2: g in x;

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

      then x in ( CCosetSet M) by Def19;

      then

      consider h be PartFunc of X, COMPLEX such that

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

      ex k be PartFunc of X, COMPLEX st f = k & k in ( L1_CFunctions M) & h in ( L1_CFunctions M) & h a.e.cpfunc= (k,M) by A1, A3;

      then

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

      ex j be PartFunc of X, COMPLEX st g = j & j in ( L1_CFunctions M) & h in ( L1_CFunctions M) & h a.e.cpfunc= (j,M) by A2, A3;

      hence thesis by A1, A3, A4, Th24;

    end;

    theorem :: LPSPACC1:40

    

     Th40: ex NORM be Function of the carrier of ( Pre-L-CSpace M), REAL st for x be Point of ( Pre-L-CSpace M) holds ex f be PartFunc of X, COMPLEX st f in x & (NORM . x) = ( Integral (M,( abs f)))

    proof

      defpred P[ set, set] means ex f be PartFunc of X, COMPLEX st f in $1 & $2 = ( Integral (M,( abs f)));

      

       A1: for x be Point of ( Pre-L-CSpace M) holds ex y be Element of REAL st P[x, y]

      proof

        let x be Point of ( Pre-L-CSpace M);

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

        then x in ( CCosetSet M) by Def19;

        then

        consider f be PartFunc of X, COMPLEX such that

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

         A3: f in ( L1_CFunctions M);

        ex f0 be PartFunc of X, COMPLEX 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 Th37;

        hence thesis by A2, A3, Th31;

      end;

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

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

      take f;

      thus thesis by A4;

    end;

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

    theorem :: LPSPACC1:41

    

     Th41: f in x implies f is_integrable_on M & f in ( L1_CFunctions M) & ( abs f) is_integrable_on M

    proof

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

      then x in ( CCosetSet M) by Def19;

      then

      consider h be PartFunc of X, COMPLEX such that

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

      assume f in x;

      then ex g be PartFunc of X, COMPLEX st f = g & g in ( L1_CFunctions M) & h in ( L1_CFunctions M) & h a.e.cpfunc= (g,M) by A1;

      then ex f0 be PartFunc of X, COMPLEX st f = f0 & ex ND be Element of S st (M . ND) = 0 & ( dom f0) = (ND ` ) & f0 is_integrable_on M;

      hence thesis by Th37;

    end;

    theorem :: LPSPACC1:42

    

     Th42: f in x & g in x implies f a.e.cpfunc= (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_CFunctions M) by A2, Th39;

      f a.e.cpfunc= (g,M) & f in ( L1_CFunctions M) by A1, A2, Th39;

      hence thesis by A3, Th36, Th38;

    end;

    definition

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

      :: LPSPACC1:def20

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

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

      existence by Th40;

      uniqueness

      proof

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

        assume

         A1: (for x be Point of ( Pre-L-CSpace M) holds ex f be PartFunc of X, COMPLEX st f in x & (N1 . x) = ( Integral (M,( abs f)))) & for x be Point of ( Pre-L-CSpace M) holds ex g be PartFunc of X, COMPLEX st g in x & (N2 . x) = ( Integral (M,( abs g)));

        now

          let x be Point of ( Pre-L-CSpace M);

          (ex f be PartFunc of X, COMPLEX st f in x & (N1 . x) = ( Integral (M,( abs f)))) & ex g be PartFunc of X, COMPLEX st g in x & (N2 . x) = ( Integral (M,( abs g))) by A1;

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

        end;

        hence N1 = N2 by FUNCT_2:def 8;

      end;

    end

    definition

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

      :: LPSPACC1:def21

      func L-1-CSpace M -> non empty CNORMSTR equals CNORMSTR (# the carrier of ( Pre-L-CSpace M), the ZeroF of ( Pre-L-CSpace M), the addF of ( Pre-L-CSpace M), the Mult of ( Pre-L-CSpace M), ( L-1-CNorm M) #);

      coherence ;

    end

    reserve x,y for Point of ( L-1-CSpace M);

    theorem :: LPSPACC1:43

    

     Th43: (ex f be PartFunc of X, COMPLEX st f in ( L1_CFunctions M) & x = ( a.e-Ceq-class (f,M)) & ||.x.|| = ( Integral (M,( abs f)))) & for f be PartFunc of X, COMPLEX st f in x holds ( Integral (M,( abs f))) = ||.x.||

    proof

      reconsider y = x as Point of ( Pre-L-CSpace M);

      consider f be PartFunc of X, COMPLEX such that

       A1: f in y and

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

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

      then y in ( CCosetSet M) by Def19;

      then

      consider g be PartFunc of X, COMPLEX such that

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

      g in y by A3, Th31;

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

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

      hence thesis by A1, A2, Th42;

    end;

    theorem :: LPSPACC1:44

    f in x implies x = ( a.e-Ceq-class (f,M)) & ||.x.|| = ( Integral (M,( abs f)))

    proof

      assume

       A1: f in x;

      reconsider y = x as Point of ( Pre-L-CSpace M);

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

      then y in ( CCosetSet M) by Def19;

      then

      consider g be PartFunc of X, COMPLEX such that

       A2: y = ( a.e-Ceq-class (g,M)) & g in ( L1_CFunctions M);

      g in y by A2, Th31;

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

      hence thesis by A1, A2, Th32, Th43;

    end;

    theorem :: LPSPACC1:45

    

     Th45: (f in x & g in y implies (f + g) in (x + y)) & (f in x implies (a (#) f) in (a * x))

    proof

      set C = ( CCosetSet M);

      hereby

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

        assume that

         A1: f in x and

         A2: g in y;

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

        then

         A3: y1 in C by Def19;

        then

        consider b be PartFunc of X, COMPLEX such that

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

         A5: b in ( L1_CFunctions M);

        

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

        ex r be PartFunc of X, COMPLEX st g = r & r in ( L1_CFunctions M) & b in ( L1_CFunctions M) & b a.e.cpfunc= (r,M) by A2, A4;

        then

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

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

        then

         A8: x1 in C by Def19;

        then

        consider a be PartFunc of X, COMPLEX such that

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

         A10: a in ( L1_CFunctions M);

        a in x1 by A9, A10, Th31;

        then (( addCCoset M) . (x1,y1)) = ( a.e-Ceq-class ((a + b),M)) by A8, A3, A6, Def16;

        then

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

        ex r be PartFunc of X, COMPLEX st f = r & r in ( L1_CFunctions M) & a in ( L1_CFunctions M) & a a.e.cpfunc= (r,M) by A1, A9;

        then ( a.e-Ceq-class (a,M)) = ( a.e-Ceq-class (f,M)) by Th32;

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

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

      end;

      hereby

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

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

        then

         A12: x1 in C by Def19;

        then

        consider f1 be PartFunc of X, COMPLEX such that

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

         A14: f1 in ( L1_CFunctions M);

        (( lmultCCoset M) . (a,x1)) = ( a.e-Ceq-class ((a (#) f1),M)) by A13, A14, Th31, A12, Def18;

        then

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

        assume

         A16: f in x;

        then ex r be PartFunc of X, COMPLEX st f = r & r in ( L1_CFunctions M) & f1 in ( L1_CFunctions M) & f1 a.e.cpfunc= (r,M) by A13;

        then ( a.e-Ceq-class (f1,M)) = ( a.e-Ceq-class (f,M)) by Th32;

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

        hence (a (#) f) in (a * x) by A16, A13, A15, Th18, Th31;

      end;

    end;

    theorem :: LPSPACC1:46

    f in ( L1_CFunctions M) & ( Integral (M,( abs f))) = 0 implies f a.e.cpfunc= ((X --> 0c ),M)

    proof

      assume that

       A1: f in ( L1_CFunctions M) and

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

      

       A3: ex f1 be PartFunc of X, COMPLEX 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

       A4: (M . NDf) = 0 and

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

      ( dom ( abs f)) = (NDf ` ) & ( abs f) is_integrable_on M by A3, A5, Th37, VALUED_1:def 11;

      then

       A6: ( abs f) in ( L1_Functions M) by A4;

      

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

      consider Ef be Element of S such that

       A8: (M . Ef) = 0 and

       A9: (( abs f) | (Ef ` )) = ((X --> 0 ) | (Ef ` )) by A6, A7, LPSPACE1: 53, LPSPACE1:def 10;

      

       A10: ( dom (X --> 0 )) = X by FUNCOP_1: 13;

      

       A11: ( dom (( abs f) | (Ef ` ))) = (( dom ( abs f)) /\ (Ef ` )) by RELAT_1: 61;

      

       A12: ( dom (f | (Ef ` ))) = (( dom f) /\ (Ef ` )) by RELAT_1: 61

      .= (( dom ( abs f)) /\ (Ef ` )) by VALUED_1:def 11

      .= ( dom (( abs f) | (Ef ` ))) by RELAT_1: 61;

      for x be object st x in ( dom (f | (Ef ` ))) holds ((f | (Ef ` )) . x) = (((X --> 0 ) | (Ef ` )) . x)

      proof

        let x be object;

        assume

         A13: x in ( dom (f | (Ef ` )));

        

         A14: x in ( dom ( abs f)) & x in (Ef ` ) by A13, A12, A11, XBOOLE_0:def 4;

        

         A15: x in ( dom ((X --> 0 ) | (Ef ` ))) by A10, RELAT_1: 62, A14;

        

         A16: (( abs f) . x) = (((X --> 0 ) | (Ef ` )) . x) by A9, A13, A12, FUNCT_1: 47

        .= ((X --> 0 ) . x) by A15, FUNCT_1: 47

        .= 0 by A13, FUNCOP_1: 7;

        

         A17: (( Re (f . x)) ^2 ) >= 0 & (( Im (f . x)) ^2 ) >= 0 by XREAL_1: 63;

        ( sqrt ((( Re (f . x)) ^2 ) + (( Im (f . x)) ^2 ))) = |.(f . x).| by COMPLEX1:def 12

        .= 0 by A16, A14, VALUED_1:def 11;

        then (( Re (f . x)) ^2 ) = 0 & (( Im (f . x)) ^2 ) = 0 by A17, SQUARE_1: 31;

        then

         A18: ((( Re (f . x)) ^2 ) + (( Im (f . x)) ^2 )) = 0 ;

        ((f | (Ef ` )) . x) = (f . x) by A13, FUNCT_1: 47

        .= 0 by A18, COMPLEX1: 5

        .= ((X --> 0 ) . x) by A13, FUNCOP_1: 7

        .= (((X --> 0 ) | (Ef ` )) . x) by A15, FUNCT_1: 47;

        hence thesis;

      end;

      hence thesis by A8, A9, A12, FUNCT_1:def 11;

    end;

    theorem :: LPSPACC1:47

    

     Th47: f in ( L1_CFunctions M) & g in ( L1_CFunctions M) implies ( Integral (M, |.(f + g).|)) <= (( Integral (M, |.f.|)) + ( Integral (M, |.g.|)))

    proof

      assume that

       A1: f in ( L1_CFunctions M) and

       A2: g in ( L1_CFunctions M);

      ex f1 be PartFunc of X, COMPLEX st f = f1 & ex NDf be Element of S st (M . NDf) = 0 & ( dom f1) = (NDf ` ) & f1 is_integrable_on M by A1;

      then

      consider NDf1 be Element of S such that

       A3: (M . NDf1) = 0 and

       A4: ( dom f) = (NDf1 ` ) & f is_integrable_on M;

      ( R_EAL |.f.|) is_integrable_on M by A4, Th37, MESFUNC6:def 4;

      then

      consider Ef be Element of S such that

       A5: Ef = ( dom ( R_EAL |.f.|)) and

       A6: ( R_EAL |.f.|) is Ef -measurable;

      ex g1 be PartFunc of X, COMPLEX st g = g1 & ex NDg be Element of S st (M . NDg) = 0 & ( dom g1) = (NDg ` ) & g1 is_integrable_on M by A2;

      then

      consider NDg1 be Element of S such that

       A7: (M . NDg1) = 0 and

       A8: ( dom g) = (NDg1 ` ) & g is_integrable_on M;

      ( R_EAL |.g.|) is_integrable_on M by A8, Th37, MESFUNC6:def 4;

      then

      consider Eg be Element of S such that

       A9: Eg = ( dom ( R_EAL |.g.|)) and

       A10: ( R_EAL |.g.|) is Eg -measurable;

      consider E be Element of S such that

       A11: E = ( dom (f + g)) & ( Integral (M,( |.(f + g).| | E))) <= (( Integral (M,( |.f.| | E))) + ( Integral (M,( |.g.| | E)))) by A4, A8, MESFUN7C: 42;

      

       A12: ( dom |.(f + g).|) = E by A11, VALUED_1:def 11;

      set NF = ((NDf1 ` ) /\ NDg1);

      set NG = ((NDg1 ` ) /\ NDf1);

      (NDf1 ` ) is Element of S & (NDg1 ` ) is Element of S by MEASURE1:def 1;

      then

       A13: NF is Element of S & NG is Element of S & Ef is Element of S & Eg is Element of S by MEASURE1: 11;

      

       A14: Ef = (NDf1 ` ) by A4, A5, VALUED_1:def 11;

      

       A15: Eg = (NDg1 ` ) by A8, A9, VALUED_1:def 11;

      then

       A16: E = (Ef /\ Eg) by A11, A14, A4, A8, VALUED_1:def 1;

      

       A17: (Ef \ Eg) = (((X \ NDf1) \ X) \/ ((X \ NDf1) /\ NDg1)) by A14, A15, XBOOLE_1: 52

      .= ((X \ (NDf1 \/ X)) \/ ((X \ NDf1) /\ NDg1)) by XBOOLE_1: 41

      .= ((X \ X) \/ ((X \ NDf1) /\ NDg1)) by XBOOLE_1: 12

      .= ( {} \/ ((X \ NDf1) /\ NDg1)) by XBOOLE_1: 37

      .= NF;

      

       A18: E = (Ef \ (Ef \ Eg)) by A16, XBOOLE_1: 48;

      

       A19: (Eg \ Ef) = (((X \ NDg1) \ X) \/ ((X \ NDg1) /\ NDf1)) by A14, A15, XBOOLE_1: 52

      .= ((X \ (NDg1 \/ X)) \/ ((X \ NDg1) /\ NDf1)) by XBOOLE_1: 41

      .= ((X \ X) \/ ((X \ NDg1) /\ NDf1)) by XBOOLE_1: 12

      .= ( {} \/ ((X \ NDg1) /\ NDf1)) by XBOOLE_1: 37

      .= NG;

      

       A20: E = (Eg \ (Eg \ Ef)) by A16, XBOOLE_1: 48;

      NDf1 is measure_zero of M & NDg1 is measure_zero of M by A3, A7, MEASURE1:def 7;

      then NF is measure_zero of M & NG is measure_zero of M by A13, MEASURE1: 36, XBOOLE_1: 17;

      then

       A21: (M . NF) = 0 & (M . NG) = 0 by MEASURE1:def 7;

      

       A22: ( Integral (M,( |.f.| | E))) = ( Integral (M, |.f.|)) by A18, A17, A6, MESFUNC6:def 1, A5, A21, MESFUNC6: 89;

      ( Integral (M,( |.g.| | E))) = ( Integral (M, |.g.|)) by A10, MESFUNC6:def 1, A9, A21, A20, A19, MESFUNC6: 89;

      hence thesis by A11, A12, RELAT_1: 69, A22;

    end;

    registration

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

      cluster ( L-1-CSpace M) -> ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        set l = ( L-1-CSpace M);

        l is ComplexNormSpace-like

        proof

          let x,y be Point of l, a be Complex;

          consider f be PartFunc of X, COMPLEX such that

           A1: f in x and

           A2: ||.x.|| = ( Integral (M,( abs f))) by Def20;

          set aa = |.a.|;

          ( abs f) is_integrable_on M by A1, Th41;

          then ( Integral (M,( |.a.| (#) ( abs f)))) = (aa * ( Integral (M,( abs f)))) by MESFUNC6: 102;

          then ( Integral (M,( abs (a (#) f)))) = (aa * ( Integral (M,( abs f)))) by RFUNCT_1: 25;

          then

           A3: ( Integral (M,( abs (a (#) f)))) = ( |.a.| * ||.x.||) by A2;

          reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;

          

           A4: f is_integrable_on M & f in ( L1_CFunctions M) by A1, Th41;

          consider g be PartFunc of X, COMPLEX such that

           A5: g in y and

           A6: ||.y.|| = ( Integral (M,( abs g))) by Def20;

          

           A7: g is_integrable_on M & g in ( L1_CFunctions M) by A5, Th41;

          

           A8: ||.(x + y).|| = ( Integral (M,( abs (f + g)))) by A1, A5, Th45, Th43;

          (a1 (#) f) in (a1 * x) by A1, Th45;

          then

           A9: ||.(a * x).|| = ( |.a.| * ||.x.||) by A3, Th43;

          (( Integral (M,( abs f))) + ( Integral (M,( abs g)))) = ( ||.x.|| + ||.y.||) by A2, A6;

          then ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by A4, A8, A7, Th47;

          hence thesis by A9;

        end;

        hence thesis by CSSPACE3: 2;

      end;

    end