:: LPSPACE1 semantic presentation

begin

definition
let V be non empty RLSStruct ;
let V1 be Subset of V;
attrV1 is multi-closed  means :Def1: :: LPSPACE1:def 1
 for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1;
end;

:: deftheorem Def1 defines multi-closed LPSPACE1:def_1_:_
 for V being non empty RLSStruct
for V1 being Subset of V holds
( V1 is multi-closed iff for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1 );

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

registration
let V be non empty RLSStruct ;
cluster non empty add-closed multi-closed for Element of bool the carrier of V;
existence
 ex b1 being Subset of V st
( b1 is add-closed & b1 is multi-closed & not b1 is empty )
proof
set M = the carrier of V;
 for u being set st u in the carrier of V holds
u in the carrier of V ;
then reconsider M = the carrier of V as Subset of V by TARSKI:def_3;
reconsider M = M as non empty Subset of V ;
take  M ; ::_thesis: ( M is add-closed & M is multi-closed & not M is empty )
 ( ( for a being Real
for v being VECTOR of V st v in M holds
a * v in M ) & ( for x, y being Element of V st x in M & y in M holds
x + y in M ) ) ;
hence  ( M is add-closed & M is multi-closed & not M is empty ) by Def1, IDEAL_1:def_1; ::_thesis: verum
end;
end;

definition
let X be non empty RLSStruct ;
let X1 be non empty multi-closed Subset of X;
func Mult_ X1 ->  Function of [:REAL,X1:],X1 equals :: LPSPACE1:def 2
 the Mult of X | [:REAL,X1:];
correctness
coherence
the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1;
proof
A1: ( [:REAL,X1:] c= [:REAL, the carrier of X:] & dom the Mult of X = [:REAL, the carrier of X:] ) by FUNCT_2:def_1, ZFMISC_1:95;
A2: now__::_thesis:_for_z_being_set_st_z_in_[:REAL,X1:]_holds_
(_the_Mult_of_X_|_[:REAL,X1:])_._z_in_X1
let z be set ; ::_thesis: ( z in [:REAL,X1:] implies ( the Mult of X | [:REAL,X1:]) . z in X1 )
assume A3: z in [:REAL,X1:] ; ::_thesis: ( the Mult of X | [:REAL,X1:]) . z in X1
then consider r, x being set  such that
A4: r in REAL and
A5: x in X1 and
A6: z = [r,x] by ZFMISC_1:def_2;
reconsider r = r as Real by A4;
reconsider y = x as VECTOR of X by A5;
 [r,x] in dom ( the Mult of X | [:REAL,X1:]) by A1, A3, A6, RELAT_1:62;
then  ( the Mult of X | [:REAL,X1:]) . z = r * y by A6, FUNCT_1:47;
hence  ( the Mult of X | [:REAL,X1:]) . z in X1 by A5, Def1; ::_thesis: verum
end;
 dom ( the Mult of X | [:REAL,X1:]) = [:REAL,X1:] by A1, RELAT_1:62;
hence  the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1 by A2, FUNCT_2:3; ::_thesis: verum
end;
end;

:: deftheorem  defines Mult_ LPSPACE1:def_2_:_
 for X being non empty RLSStruct
for X1 being non empty multi-closed Subset of X holds Mult_ X1 = the Mult of X | [:REAL,X1:];


theorem Th2: :: LPSPACE1:2
for V being non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for V1 being non empty Subset of V
for d1 being Element of V1
for A being BinOp of V1
for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
proof
let V be non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for V1 being non empty Subset of V
for d1 being Element of V1
for A being BinOp of V1
for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let V1 be non empty Subset of V; ::_thesis: for d1 being Element of V1
for A being BinOp of V1
for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let d1 be Element of V1; ::_thesis: for A being BinOp of V1
for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let A be BinOp of V1; ::_thesis: for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let M be Function of [:REAL,V1:],V1; ::_thesis: ( d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] implies ( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital ) )
set D = V1;
assume that
A1: d1 = 0. V and
A2: A = the addF of V || V1 and
A3: M = the Mult of V | [:REAL,V1:] ; ::_thesis: ( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
set W = RLSStruct(# V1,d1,A,M #);
A4: now__::_thesis:_for_a_being_Real
for_x_being_VECTOR_of_RLSStruct(#_V1,d1,A,M_#)_holds_a_*_x_=_the_Mult_of_V_._(a,x)
let a be Real; ::_thesis: for x being VECTOR of RLSStruct(# V1,d1,A,M #) holds a * x = the Mult of V . (a,x)
let x be VECTOR of RLSStruct(# V1,d1,A,M #); ::_thesis: a * x = the Mult of V . (a,x)
thus a * x = the Mult of V . [a,x] by A3, FUNCT_1:49
.= the Mult of V . (a,x) ; ::_thesis: verum
end;
A5: now__::_thesis:_for_x,_y_being_VECTOR_of_RLSStruct(#_V1,d1,A,M_#)_holds_x_+_y_=_the_addF_of_V_._(x,y)
let x, y be VECTOR of RLSStruct(# V1,d1,A,M #); ::_thesis: x + y = the addF of V . (x,y)
thus x + y = the addF of V . [x,y] by A2, FUNCT_1:49
.= the addF of V . (x,y) ; ::_thesis: verum
end;
 ( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
proof
set Mv = the Mult of V;
set Av = the addF of V;
hereby  :: according to RLVECT_1:def_2 ::_thesis: ( RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let x, y be VECTOR of RLSStruct(# V1,d1,A,M #); ::_thesis: x + y = y + x
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 ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_VECTOR_of_RLSStruct(#_V1,d1,A,M_#)_holds_(x_+_y)_+_z_=_x_+_(y_+_z)
let x, y, z be VECTOR of RLSStruct(# V1,d1,A,M #); ::_thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by TARSKI:def_3;
thus (x + y) + z = the addF of V . ((x + y),z1) by A5
.= (x1 + y1) + z1 by A5
.= x1 + (y1 + z1) by RLVECT_1:def_3
.= the addF of V . (x1,(y + z)) by A5
.= x + (y + z) by A5 ; ::_thesis: verum
end;
hence  RLSStruct(# V1,d1,A,M #) is add-associative by RLVECT_1:def_3; ::_thesis: ( RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
now__::_thesis:_for_x_being_VECTOR_of_RLSStruct(#_V1,d1,A,M_#)_holds_x_+_(0._RLSStruct(#_V1,d1,A,M_#))_=_x
let x be VECTOR of RLSStruct(# V1,d1,A,M #); ::_thesis: x + (0. RLSStruct(# V1,d1,A,M #)) = x
reconsider y = x as VECTOR of V by TARSKI:def_3;
thus x + (0. RLSStruct(# V1,d1,A,M #)) = y + (0. V) by A1, A5
.= x by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence  RLSStruct(# V1,d1,A,M #) is right_zeroed by RLVECT_1:def_4; ::_thesis: ( RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
hereby  :: according to RLVECT_1:def_5 ::_thesis: ( RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let a1 be real number ; ::_thesis: for x, y being VECTOR of RLSStruct(# V1,d1,A,M #) holds a1 * (x + y) = (a1 * x) + (a1 * y)
let x, y be VECTOR of RLSStruct(# V1,d1,A,M #); ::_thesis: a1 * (x + y) = (a1 * x) + (a1 * y)
reconsider a = a1 as Real by XREAL_0:def_1;
reconsider x1 = x, y1 = y as VECTOR of V by TARSKI:def_3;
a * (x + y) = the Mult of V . (a,(x + y)) by A4
.= a * (x1 + y1) by A5
.= (a * x1) + (a * y1) by RLVECT_1:def_5
.= the addF of V . (( the Mult of V . (a,x1)),(a * y)) by A4
.= the addF of V . ((a * x),(a * y)) by A4
.= (a * x) + (a * y) by A5 ;
hence  a1 * (x + y) = (a1 * x) + (a1 * y) ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_6 ::_thesis: ( RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let a1, b1 be real number ; ::_thesis: for x being VECTOR of RLSStruct(# V1,d1,A,M #) holds (a1 + b1) * x = (a1 * x) + (b1 * x)
let x be VECTOR of RLSStruct(# V1,d1,A,M #); ::_thesis: (a1 + b1) * x = (a1 * x) + (b1 * x)
reconsider a = a1, b = b1 as Real by XREAL_0:def_1;
reconsider y = x as VECTOR of V by TARSKI:def_3;
(a + b) * x = (a + b) * y by A4
.= (a * y) + (b * y) by RLVECT_1:def_6
.= the addF of V . (( the Mult of V . (a,y)),(b * x)) by A4
.= the addF of V . ((a * x),(b * x)) by A4
.= (a * x) + (b * x) by A5 ;
hence  (a1 + b1) * x = (a1 * x) + (b1 * x) ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_7 ::_thesis: RLSStruct(# V1,d1,A,M #) is scalar-unital
let a1, b1 be real number ; ::_thesis: for x being VECTOR of RLSStruct(# V1,d1,A,M #) holds (a1 * b1) * x = a1 * (b1 * x)
let x be VECTOR of RLSStruct(# V1,d1,A,M #); ::_thesis: (a1 * b1) * x = a1 * (b1 * x)
reconsider a = a1, b = b1 as Real by XREAL_0:def_1;
reconsider y = x as VECTOR of V by TARSKI:def_3;
(a * b) * x = (a * b) * y by A4
.= a * (b * y) by RLVECT_1:def_7
.= the Mult of V . (a,(b * x)) by A4
.= a * (b * x) by A4 ;
hence  (a1 * b1) * x = a1 * (b1 * x) ; ::_thesis: verum
end;
let x be VECTOR of RLSStruct(# V1,d1,A,M #); :: according to RLVECT_1:def_8 ::_thesis: 1 * x = x
reconsider y = x as VECTOR of V by TARSKI:def_3;
thus 1 * x = 1 * y by A4
.= x by RLVECT_1:def_8 ; ::_thesis: verum
end;
hence  ( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital ) ; ::_thesis: verum
end;

theorem Th3: :: LPSPACE1:3
for V being non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for V1 being non empty add-closed multi-closed Subset of V st 0. V in V1 holds
( RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is Abelian & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is add-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is right_zeroed & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is vector-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-unital )
proof
let V be non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for V1 being non empty add-closed multi-closed Subset of V st 0. V in V1 holds
( RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is Abelian & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is add-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is right_zeroed & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is vector-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-unital )
let V1 be non empty add-closed multi-closed Subset of V; ::_thesis: ( 0. V in V1 implies ( RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is Abelian & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is add-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is right_zeroed & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is vector-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-unital ) )
assume  0. V in V1 ; ::_thesis: ( RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is Abelian & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is add-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is right_zeroed & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is vector-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-unital )
then  In ((0. V),V1) = 0. V by FUNCT_7:def_1;
hence  ( RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is Abelian & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is add-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is right_zeroed & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is vector-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-unital ) by Th2; ::_thesis: verum
end;

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

theorem Th5: :: LPSPACE1:5
for V being non empty RLSStruct
for V1 being non empty add-closed multi-closed Subset of V
for a being Real
for v being VECTOR of V
for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v
proof
let V be non empty RLSStruct ; ::_thesis: for V1 being non empty add-closed multi-closed Subset of V
for a being Real
for v being VECTOR of V
for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v
let V1 be non empty add-closed multi-closed Subset of V; ::_thesis: for a being Real
for v being VECTOR of V
for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v
let a be Real; ::_thesis: for v being VECTOR of V
for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v
let v be VECTOR of V; ::_thesis: for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v
let w be VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #); ::_thesis: ( w = v implies a * w = a * v )
assume A1: w = v ; ::_thesis: a * w = a * v
then  [a,v] in [:REAL,V1:] by ZFMISC_1:87;
hence  a * w = a * v by A1, FUNCT_1:49; ::_thesis: verum
end;

begin


definition
let A, B be non empty set ;
let F be BinOp of (PFuncs (A,B));
let f, g be Element of PFuncs (A,B);
:: original: .
redefine funcF . (f,g) ->  Element of PFuncs (A,B);
coherence
 F . (f,g) is Element of PFuncs (A,B)
proof
reconsider f = f, g = g as Element of PFuncs (A,B) ;
 F . (f,g) is Element of PFuncs (A,B) ;
hence  F . (f,g) is Element of PFuncs (A,B) ; ::_thesis: verum
end;
end;

definition
let A be non empty set ;
func multpfunc A ->  BinOp of (PFuncs (A,REAL)) means :Def3: :: LPSPACE1:def 3
 for f, g being Element of PFuncs (A,REAL) holds it . (f,g) = f (#) g;
existence
 ex b1 being BinOp of (PFuncs (A,REAL)) st
for f, g being Element of PFuncs (A,REAL) holds b1 . (f,g) = f (#) g
proof
deffunc H1( Element of PFuncs (A,REAL), Element of PFuncs (A,REAL)) ->  Element of PFuncs (A,REAL) = $1 (#) $2;
 ex F being BinOp of (PFuncs (A,REAL)) st
for f, g being Element of PFuncs (A,REAL) holds F . (f,g) = H1(f,g) from BINOP_1:sch_4();
hence  ex b1 being BinOp of (PFuncs (A,REAL)) st
for f, g being Element of PFuncs (A,REAL) holds b1 . (f,g) = f (#) g ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (PFuncs (A,REAL)) st ( for f, g being Element of PFuncs (A,REAL) holds b1 . (f,g) = f (#) g ) & ( for f, g being Element of PFuncs (A,REAL) holds b2 . (f,g) = f (#) g ) holds
b1 = b2
proof
let it1, it2 be BinOp of (PFuncs (A,REAL)); ::_thesis: ( ( for f, g being Element of PFuncs (A,REAL) holds it1 . (f,g) = f (#) g ) & ( for f, g being Element of PFuncs (A,REAL) holds it2 . (f,g) = f (#) g ) implies it1 = it2 )
assume that
A1: for f, g being Element of PFuncs (A,REAL) holds it1 . (f,g) = f (#) g and
A2: for f, g being Element of PFuncs (A,REAL) holds it2 . (f,g) = f (#) g ; ::_thesis: it1 = it2
now__::_thesis:_for_f,_g_being_Element_of_PFuncs_(A,REAL)_holds_it1_._(f,g)_=_it2_._(f,g)
let f, g be Element of PFuncs (A,REAL); ::_thesis: it1 . (f,g) = it2 . (f,g)
thus it1 . (f,g) = f (#) g by A1
.= it2 . (f,g) by A2 ; ::_thesis: verum
end;
hence  it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines multpfunc LPSPACE1:def_3_:_
 for A being non empty set
for b2 being BinOp of (PFuncs (A,REAL)) holds
( b2 = multpfunc A iff for f, g being Element of PFuncs (A,REAL) holds b2 . (f,g) = f (#) g );

definition
let A be non empty set ;
func multrealpfunc A ->  Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) means :Def4: :: LPSPACE1:def 4
 for a being Real
for f being Element of PFuncs (A,REAL) holds it . (a,f) = a (#) f;
existence
 ex b1 being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) st
for a being Real
for f being Element of PFuncs (A,REAL) holds b1 . (a,f) = a (#) f
proof
deffunc H1( Element of REAL , Element of PFuncs (A,REAL)) ->  Element of PFuncs (A,REAL) = $1 (#) $2;
 ex F being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) st
for a being Real
for f being Element of PFuncs (A,REAL) holds F . (a,f) = H1(a,f) from BINOP_1:sch_4();
hence  ex b1 being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) st
for a being Real
for f being Element of PFuncs (A,REAL) holds b1 . (a,f) = a (#) f ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) st ( for a being Real
for f being Element of PFuncs (A,REAL) holds b1 . (a,f) = a (#) f ) & ( for a being Real
for f being Element of PFuncs (A,REAL) holds b2 . (a,f) = a (#) f ) holds
b1 = b2
proof
let it1, it2 be Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)); ::_thesis: ( ( for a being Real
for f being Element of PFuncs (A,REAL) holds it1 . (a,f) = a (#) f ) & ( for a being Real
for f being Element of PFuncs (A,REAL) holds it2 . (a,f) = a (#) f ) implies it1 = it2 )
assume that
A1: for a being Real
for f being Element of PFuncs (A,REAL) holds it1 . (a,f) = a (#) f and
A2: for a being Real
for f being Element of PFuncs (A,REAL) holds it2 . (a,f) = a (#) f ; ::_thesis: it1 = it2
now__::_thesis:_for_a_being_Element_of_REAL_
for_f_being_Element_of_PFuncs_(A,REAL)_holds_it1_._(a,f)_=_it2_._(a,f)
let a be Element of REAL ; ::_thesis: for f being Element of PFuncs (A,REAL) holds it1 . (a,f) = it2 . (a,f)
let f be Element of PFuncs (A,REAL); ::_thesis: it1 . (a,f) = it2 . (a,f)
thus it1 . (a,f) = a (#) f by A1
.= it2 . (a,f) by A2 ; ::_thesis: verum
end;
hence  it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines multrealpfunc LPSPACE1:def_4_:_
 for A being non empty set
for b2 being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) holds
( b2 = multrealpfunc A iff for a being Real
for f being Element of PFuncs (A,REAL) holds b2 . (a,f) = a (#) f );

definition
let A be non empty set ;
func RealPFuncZero A ->  Element of PFuncs (A,REAL) equals :: LPSPACE1:def 5
A --> 0;
coherence
 A --> 0 is Element of PFuncs (A,REAL)
proof
 A --> 0 is Function of A,REAL by FUNCOP_1:46;
hence  A --> 0 is Element of PFuncs (A,REAL) by PARTFUN1:45; ::_thesis: verum
end;
end;

:: deftheorem  defines RealPFuncZero LPSPACE1:def_5_:_
 for A being non empty set holds RealPFuncZero A = A --> 0;

definition
let A be non empty set ;
func RealPFuncUnit A ->  Element of PFuncs (A,REAL) equals :: LPSPACE1:def 6
A --> 1;
coherence
 A --> 1 is Element of PFuncs (A,REAL)
proof
 A --> 1 is Function of A,REAL by FUNCOP_1:46;
hence  A --> 1 is Element of PFuncs (A,REAL) by PARTFUN1:45; ::_thesis: verum
end;
end;

:: deftheorem  defines RealPFuncUnit LPSPACE1:def_6_:_
 for A being non empty set holds RealPFuncUnit A = A --> 1;

theorem Th6: :: LPSPACE1:6
for A being non empty set
for h, f, g being Element of PFuncs (A,REAL) holds
( h = (addpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) ) )
proof
let A be non empty set ; ::_thesis: for h, f, g being Element of PFuncs (A,REAL) holds
( h = (addpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) ) )
let h, f, g be Element of PFuncs (A,REAL); ::_thesis: ( h = (addpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) ) )
hereby  ::_thesis: ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) implies h = (addpfunc A) . (f,g) )
assume A1: h = (addpfunc A) . (f,g) ; ::_thesis: ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) )
then  dom h = dom (f + g) by RFUNCT_3:def_4;
hence  dom h = (dom f) /\ (dom g) by VALUED_1:def_1; ::_thesis: for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x)
let x be Element of A; ::_thesis: ( x in dom h implies h . x = (f . x) + (g . x) )
assume  x in dom h ; ::_thesis: h . x = (f . x) + (g . x)
then A2: x in dom (f + g) by A1, RFUNCT_3:def_4;
 h . x = (f + g) . x by A1, RFUNCT_3:def_4;
hence  h . x = (f . x) + (g . x) by A2, VALUED_1:def_1; ::_thesis: verum
end;
assume that
A3: dom h = (dom f) /\ (dom g) and
A4: for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ; ::_thesis: h = (addpfunc A) . (f,g)
set k = (addpfunc A) . (f,g);
A5: now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_h_holds_
((addpfunc_A)_._(f,g))_._x_=_h_._x
let x be Element of A; ::_thesis: ( x in dom h implies ((addpfunc A) . (f,g)) . x = h . x )
A6: ((addpfunc A) . (f,g)) . x = (f + g) . x by RFUNCT_3:def_4;
assume A7: x in dom h ; ::_thesis: ((addpfunc A) . (f,g)) . x = h . x
then  x in dom (f + g) by A3, VALUED_1:def_1;
hence ((addpfunc A) . (f,g)) . x = (f . x) + (g . x) by A6, VALUED_1:def_1
.= h . x by A4, A7 ;
::_thesis: verum
end;
dom ((addpfunc A) . (f,g)) = dom (f + g) by RFUNCT_3:def_4
.= dom h by A3, VALUED_1:def_1 ;
hence  h = (addpfunc A) . (f,g) by A5, PARTFUN1:5; ::_thesis: verum
end;

theorem Th7: :: LPSPACE1:7
for A being non empty set
for h, f, g being Element of PFuncs (A,REAL) holds
( h = (multpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) ) )
proof
let A be non empty set ; ::_thesis: for h, f, g being Element of PFuncs (A,REAL) holds
( h = (multpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) ) )
let h, f, g be Element of PFuncs (A,REAL); ::_thesis: ( h = (multpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) ) )
set k = (multpfunc A) . (f,g);
hereby  ::_thesis: ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) implies h = (multpfunc A) . (f,g) )
assume A1: h = (multpfunc A) . (f,g) ; ::_thesis: ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) )
hence  dom h = dom (f (#) g) by Def3
.= (dom f) /\ (dom g) by VALUED_1:def_4 ;
::_thesis: for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x)
let x be Element of A; ::_thesis: ( x in dom h implies h . x = (f . x) * (g . x) )
assume  x in dom h ; ::_thesis: h . x = (f . x) * (g . x)
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; ::_thesis: verum
end;
assume that
A3: dom h = (dom f) /\ (dom g) and
A4: for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ; ::_thesis: h = (multpfunc A) . (f,g)
A5: now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_h_holds_
((multpfunc_A)_._(f,g))_._x_=_h_._x
let x be Element of A; ::_thesis: ( x in dom h implies ((multpfunc A) . (f,g)) . x = h . x )
A6: ((multpfunc A) . (f,g)) . x = (f (#) g) . x by Def3;
assume A7: x in dom h ; ::_thesis: ((multpfunc A) . (f,g)) . x = h . x
then  x in dom (f (#) g) by A3, VALUED_1:def_4;
hence ((multpfunc A) . (f,g)) . x = (f . x) * (g . x) by A6, VALUED_1:def_4
.= h . x by A4, A7 ;
::_thesis: verum
end;
dom ((multpfunc A) . (f,g)) = dom (f (#) g) by Def3
.= dom h by A3, VALUED_1:def_4 ;
hence  h = (multpfunc A) . (f,g) by A5, PARTFUN1:5; ::_thesis: verum
end;

theorem :: LPSPACE1:8
for A being non empty set holds RealPFuncZero A <> RealPFuncUnit A
proof
let A be non empty set ; ::_thesis: RealPFuncZero A <> RealPFuncUnit A
set a = the Element of A;
 (RealPFuncZero A) . the Element of A = 0 by FUNCOP_1:7;
hence  RealPFuncZero A <> RealPFuncUnit A by FUNCOP_1:7; ::_thesis: verum
end;

theorem Th9: :: LPSPACE1:9
for a being Real
for A being non empty set
for h, f being Element of PFuncs (A,REAL) holds
( h = (multrealpfunc A) . (a,f) iff ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )
proof
let a be Real; ::_thesis: for A being non empty set
for h, f being Element of PFuncs (A,REAL) holds
( h = (multrealpfunc A) . (a,f) iff ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )
let A be non empty set ; ::_thesis: for h, f being Element of PFuncs (A,REAL) holds
( h = (multrealpfunc A) . (a,f) iff ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )
let h, f be Element of PFuncs (A,REAL); ::_thesis: ( h = (multrealpfunc A) . (a,f) iff ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )
hereby  ::_thesis: ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) implies h = (multrealpfunc A) . (a,f) )
assume A1: h = (multrealpfunc A) . (a,f) ; ::_thesis: ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) )
then  dom h = dom (a (#) f) by Def4;
hence  dom h = dom f by VALUED_1:def_5; ::_thesis: for x being Element of A st x in dom f holds
h . x = a * (f . x)
let x be Element of A; ::_thesis: ( x in dom f implies h . x = a * (f . x) )
assume  x in dom f ; ::_thesis: h . x = a * (f . x)
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; ::_thesis: verum
end;
hereby  ::_thesis: verum
reconsider k = (multrealpfunc A) . (a,f) as Element of PFuncs (A,REAL) ;
assume that
A2: dom f = dom h and
A3: for x being Element of A st x in dom f holds
h . x = a * (f . x) ; ::_thesis: h = (multrealpfunc A) . (a,f)
A4: now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_f_holds_
k_._x_=_h_._x
let x be Element of A; ::_thesis: ( x in dom f implies k . x = h . x )
assume A5: x in dom f ; ::_thesis: k . x = h . x
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; ::_thesis: verum
end;
 k = a (#) f by Def4;
then  dom k = dom f by VALUED_1:def_5;
hence  h = (multrealpfunc A) . (a,f) by A2, A4, PARTFUN1:5; ::_thesis: verum
end;
end;

theorem Th10: :: LPSPACE1:10
for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,g) = (addpfunc A) . (g,f)
proof
let A be non empty set ; ::_thesis: for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,g) = (addpfunc A) . (g,f)
let f, g be Element of PFuncs (A,REAL); ::_thesis: (addpfunc A) . (f,g) = (addpfunc A) . (g,f)
 addpfunc A is commutative by RFUNCT_3:14;
hence  (addpfunc A) . (f,g) = (addpfunc A) . (g,f) by BINOP_1:def_2; ::_thesis: verum
end;

theorem Th11: :: LPSPACE1:11
for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((addpfunc A) . (f,g)),h)
proof
let A be non empty set ; ::_thesis: for f, g, h being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((addpfunc A) . (f,g)),h)
let f, g, h be Element of PFuncs (A,REAL); ::_thesis: (addpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((addpfunc A) . (f,g)),h)
 addpfunc A is associative by RFUNCT_3:15;
hence  (addpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((addpfunc A) . (f,g)),h) by BINOP_1:def_3; ::_thesis: verum
end;

theorem :: LPSPACE1:12
for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,g) = (multpfunc A) . (g,f)
proof
let A be non empty set ; ::_thesis: for f, g being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,g) = (multpfunc A) . (g,f)
let f, g be Element of PFuncs (A,REAL); ::_thesis: (multpfunc A) . (f,g) = (multpfunc A) . (g,f)
A1: dom ((multpfunc A) . (g,f)) = (dom g) /\ (dom f) by Th7;
A2: dom ((multpfunc A) . (f,g)) = (dom f) /\ (dom g) by Th7;
now__::_thesis:_for_x_being_Element_of_A_st_x_in_(dom_f)_/\_(dom_g)_holds_
((multpfunc_A)_._(f,g))_._x_=_((multpfunc_A)_._(g,f))_._x
let x be Element of A; ::_thesis: ( x in (dom f) /\ (dom g) implies ((multpfunc A) . (f,g)) . x = ((multpfunc A) . (g,f)) . x )
assume A3: x in (dom f) /\ (dom g) ; ::_thesis: ((multpfunc A) . (f,g)) . x = ((multpfunc A) . (g,f)) . x
hence ((multpfunc A) . (f,g)) . x = (g . x) * (f . x) by A2, Th7
.= ((multpfunc A) . (g,f)) . x by A1, A3, Th7 ;
::_thesis: verum
end;
hence  (multpfunc A) . (f,g) = (multpfunc A) . (g,f) by A2, A1, PARTFUN1:5; ::_thesis: verum
end;

theorem :: LPSPACE1:13
for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,((multpfunc A) . (g,h))) = (multpfunc A) . (((multpfunc A) . (f,g)),h)
proof
let A be non empty set ; ::_thesis: for f, g, h being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,((multpfunc A) . (g,h))) = (multpfunc A) . (((multpfunc A) . (f,g)),h)
let f, g, h be Element of PFuncs (A,REAL); ::_thesis: (multpfunc A) . (f,((multpfunc A) . (g,h))) = (multpfunc A) . (((multpfunc A) . (f,g)),h)
set j = (multpfunc A) . (g,h);
set k = (multpfunc A) . (f,g);
set j1 = (multpfunc A) . (f,((multpfunc A) . (g,h)));
set k1 = (multpfunc A) . (((multpfunc A) . (f,g)),h);
A1: dom ((multpfunc A) . (((multpfunc A) . (f,g)),h)) = (dom ((multpfunc A) . (f,g))) /\ (dom h) by Th7;
then A2: dom ((multpfunc A) . (((multpfunc A) . (f,g)),h)) c= dom ((multpfunc A) . (f,g)) by XBOOLE_1:17;
A3: dom ((multpfunc A) . (((multpfunc A) . (f,g)),h)) = ((dom f) /\ (dom g)) /\ (dom h) by A1, Th7;
A4: dom ((multpfunc A) . (f,((multpfunc A) . (g,h)))) = (dom f) /\ (dom ((multpfunc A) . (g,h))) by Th7;
then A5: dom ((multpfunc A) . (f,((multpfunc A) . (g,h)))) = (dom f) /\ ((dom g) /\ (dom h)) by Th7;
A6: dom ((multpfunc A) . (f,((multpfunc A) . (g,h)))) c= dom ((multpfunc A) . (g,h)) by A4, XBOOLE_1:17;
now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_((multpfunc_A)_._(f,((multpfunc_A)_._(g,h))))_holds_
((multpfunc_A)_._(f,((multpfunc_A)_._(g,h))))_._x_=_((multpfunc_A)_._(((multpfunc_A)_._(f,g)),h))_._x
let x be Element of A; ::_thesis: ( x in dom ((multpfunc A) . (f,((multpfunc A) . (g,h)))) implies ((multpfunc A) . (f,((multpfunc A) . (g,h)))) . x = ((multpfunc A) . (((multpfunc A) . (f,g)),h)) . x )
assume A7: x in dom ((multpfunc A) . (f,((multpfunc A) . (g,h)))) ; ::_thesis: ((multpfunc A) . (f,((multpfunc A) . (g,h)))) . x = ((multpfunc A) . (((multpfunc A) . (f,g)),h)) . x
then A8: x in dom ((multpfunc A) . (((multpfunc A) . (f,g)),h)) by A5, A3, XBOOLE_1:16;
thus ((multpfunc A) . (f,((multpfunc A) . (g,h)))) . x = (f . x) * (((multpfunc A) . (g,h)) . x) by A7, Th7
.= (f . x) * ((g . x) * (h . x)) by A6, A7, Th7
.= ((f . x) * (g . x)) * (h . x)
.= (((multpfunc A) . (f,g)) . x) * (h . x) by A2, A8, Th7
.= ((multpfunc A) . (((multpfunc A) . (f,g)),h)) . x by A8, Th7 ; ::_thesis: verum
end;
hence  (multpfunc A) . (f,((multpfunc A) . (g,h))) = (multpfunc A) . (((multpfunc A) . (f,g)),h) by A5, A3, PARTFUN1:5, XBOOLE_1:16; ::_thesis: verum
end;

theorem :: LPSPACE1:14
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multpfunc A) . ((RealPFuncUnit A),f) = f
proof
let A be non empty set ; ::_thesis: for f being Element of PFuncs (A,REAL) holds (multpfunc A) . ((RealPFuncUnit A),f) = f
let f be Element of PFuncs (A,REAL); ::_thesis: (multpfunc A) . ((RealPFuncUnit A),f) = f
set h = (multpfunc A) . ((RealPFuncUnit A),f);
 dom ((multpfunc A) . ((RealPFuncUnit A),f)) = (dom (RealPFuncUnit A)) /\ (dom f) by Th7;
then  dom ((multpfunc A) . ((RealPFuncUnit A),f)) = A /\ (dom f) by FUNCOP_1:13;
then A1: dom ((multpfunc A) . ((RealPFuncUnit A),f)) = dom f by XBOOLE_1:28;
now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_f_holds_
((multpfunc_A)_._((RealPFuncUnit_A),f))_._x_=_f_._x
let x be Element of A; ::_thesis: ( x in dom f implies ((multpfunc A) . ((RealPFuncUnit A),f)) . x = f . x )
assume  x in dom f ; ::_thesis: ((multpfunc A) . ((RealPFuncUnit A),f)) . x = f . x
then  ((multpfunc A) . ((RealPFuncUnit A),f)) . x = ((RealPFuncUnit A) . x) * (f . x) by A1, Th7;
then  ((multpfunc A) . ((RealPFuncUnit A),f)) . x = 1 * (f . x) by FUNCOP_1:7;
hence  ((multpfunc A) . ((RealPFuncUnit A),f)) . x = f . x ; ::_thesis: verum
end;
hence  (multpfunc A) . ((RealPFuncUnit A),f) = f by A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th15: :: LPSPACE1:15
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . ((RealPFuncZero A),f) = f
proof
let A be non empty set ; ::_thesis: for f being Element of PFuncs (A,REAL) holds (addpfunc A) . ((RealPFuncZero A),f) = f
let f be Element of PFuncs (A,REAL); ::_thesis: (addpfunc A) . ((RealPFuncZero A),f) = f
set h = (addpfunc A) . ((RealPFuncZero A),f);
 dom ((addpfunc A) . ((RealPFuncZero A),f)) = (dom (RealPFuncZero A)) /\ (dom f) by Th6;
then  dom ((addpfunc A) . ((RealPFuncZero A),f)) = A /\ (dom f) by FUNCOP_1:13;
then A1: dom ((addpfunc A) . ((RealPFuncZero A),f)) = dom f by XBOOLE_1:28;
now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_f_holds_
((addpfunc_A)_._((RealPFuncZero_A),f))_._x_=_f_._x
let x be Element of A; ::_thesis: ( x in dom f implies ((addpfunc A) . ((RealPFuncZero A),f)) . x = f . x )
A2: (RealPFuncZero A) . x = 0 by FUNCOP_1:7;
assume  x in dom f ; ::_thesis: ((addpfunc A) . ((RealPFuncZero A),f)) . x = f . x
hence ((addpfunc A) . ((RealPFuncZero A),f)) . x = 0 + (f . x) by A1, A2, Th6
.= f . x ;
::_thesis: verum
end;
hence  (addpfunc A) . ((RealPFuncZero A),f) = f by A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th16: :: LPSPACE1:16
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((multrealpfunc A) . ((- 1),f))) = (RealPFuncZero A) | (dom f)
proof
let A be non empty set ; ::_thesis: for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((multrealpfunc A) . ((- 1),f))) = (RealPFuncZero A) | (dom f)
let f be Element of PFuncs (A,REAL); ::_thesis: (addpfunc A) . (f,((multrealpfunc A) . ((- 1),f))) = (RealPFuncZero A) | (dom f)
reconsider g = (multrealpfunc A) . ((- 1),f) as Element of PFuncs (A,REAL) ;
set h = (addpfunc A) . (f,g);
 dom (RealPFuncZero A) = A by FUNCOP_1:13;
then  dom ((RealPFuncZero A) | (dom f)) = A /\ (dom f) by RELAT_1:61;
then A1: dom ((RealPFuncZero A) | (dom f)) = dom f by XBOOLE_1:28;
A2: dom ((addpfunc A) . (f,g)) = (dom g) /\ (dom f) by Th6
.= (dom f) /\ (dom f) by Th9 ;
now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_f_holds_
((addpfunc_A)_._(f,g))_._x_=_((RealPFuncZero_A)_|_(dom_f))_._x
let x be Element of A; ::_thesis: ( x in dom f implies ((addpfunc A) . (f,g)) . x = ((RealPFuncZero A) | (dom f)) . x )
assume A3: x in dom f ; ::_thesis: ((addpfunc A) . (f,g)) . x = ((RealPFuncZero A) | (dom f)) . x
then A4: x in dom ((- 1) (#) f) by VALUED_1:def_5;
thus ((addpfunc A) . (f,g)) . x = (f . x) + (g . x) by A2, A3, Th6
.= (f . x) + (((- 1) (#) f) . x) by Def4
.= (f . x) + ((- 1) * (f . x)) by A4, VALUED_1:def_5
.= (RealPFuncZero A) . x by FUNCOP_1:7
.= ((RealPFuncZero A) | (dom f)) . x by A3, FUNCT_1:49 ; ::_thesis: verum
end;
hence  (addpfunc A) . (f,((multrealpfunc A) . ((- 1),f))) = (RealPFuncZero A) | (dom f) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;

theorem Th17: :: LPSPACE1:17
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (1,f) = f
proof
let A be non empty set ; ::_thesis: for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (1,f) = f
let f be Element of PFuncs (A,REAL); ::_thesis: (multrealpfunc A) . (1,f) = f
reconsider g = (multrealpfunc A) . (1,f) as Element of PFuncs (A,REAL) ;
A1: now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_f_holds_
g_._x_=_f_._x
let x be Element of A; ::_thesis: ( x in dom f implies g . x = f . x )
assume  x in dom f ; ::_thesis: g . x = f . x
hence g . x = 1 * (f . x) by Th9
.= f . x ;
::_thesis: verum
end;
 dom g = dom f by Th9;
hence  (multrealpfunc A) . (1,f) = f by A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th18: :: LPSPACE1:18
for a, b being Real
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f)
proof
let a, b be Real; ::_thesis: for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f)
let A be non empty set ; ::_thesis: for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f)
let f be Element of PFuncs (A,REAL); ::_thesis: (multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f)
reconsider g = (multrealpfunc A) . (b,f) as Element of PFuncs (A,REAL) ;
reconsider h = (multrealpfunc A) . (a,g) as Element of PFuncs (A,REAL) ;
reconsider k = (multrealpfunc A) . ((a * b),f) as Element of PFuncs (A,REAL) ;
A1: dom h = dom g by Th9;
A2: dom g = dom f by Th9;
A3: now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_h_holds_
h_._x_=_k_._x
let x be Element of A; ::_thesis: ( x in dom h implies h . x = k . x )
assume A4: x in dom h ; ::_thesis: h . x = k . x
hence h . x = a * (g . x) by A1, Th9
.= a * (b * (f . x)) by A2, A1, A4, Th9
.= (a * b) * (f . x)
.= k . x by A2, A1, A4, Th9 ;
::_thesis: verum
end;
 dom k = dom f by Th9;
hence  (multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f) by A2, A1, A3, PARTFUN1:5; ::_thesis: verum
end;

theorem Th19: :: LPSPACE1:19
for a, b being Real
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a + b),f)
proof
let a, b be Real; ::_thesis: for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a + b),f)
let A be non empty set ; ::_thesis: for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a + b),f)
let f be Element of PFuncs (A,REAL); ::_thesis: (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a + b),f)
reconsider g = (multrealpfunc A) . (a,f) as Element of PFuncs (A,REAL) ;
reconsider h = (multrealpfunc A) . (b,f) as Element of PFuncs (A,REAL) ;
reconsider k = (multrealpfunc A) . ((a + b),f) as Element of PFuncs (A,REAL) ;
set j = (addpfunc A) . (g,h);
 dom g = dom f by Th9;
then  (dom h) /\ (dom g) = (dom f) /\ (dom f) by Th9;
then A1: dom ((addpfunc A) . (g,h)) = dom f by Th6;
A2: now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_((addpfunc_A)_._(g,h))_holds_
((addpfunc_A)_._(g,h))_._x_=_k_._x
let x be Element of A; ::_thesis: ( x in dom ((addpfunc A) . (g,h)) implies ((addpfunc A) . (g,h)) . x = k . x )
assume A3: x in dom ((addpfunc A) . (g,h)) ; ::_thesis: ((addpfunc A) . (g,h)) . x = k . x
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 ((addpfunc A) . (g,h)) . x = (a + b) * (f . x) by A3, Th6
.= k . x by A1, A3, Th9 ;
::_thesis: verum
end;
 dom k = dom f by Th9;
hence  (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a + b),f) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;

Lm1:  for a being Real
for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (a,g))) = (multrealpfunc A) . (a,((addpfunc A) . (f,g)))
proof
let a be Real; ::_thesis: for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (a,g))) = (multrealpfunc A) . (a,((addpfunc A) . (f,g)))
let A be non empty set ; ::_thesis: for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (a,g))) = (multrealpfunc A) . (a,((addpfunc A) . (f,g)))
let f, g be Element of PFuncs (A,REAL); ::_thesis: (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (a,g))) = (multrealpfunc A) . (a,((addpfunc A) . (f,g)))
reconsider h = (multrealpfunc A) . (a,f) as Element of PFuncs (A,REAL) ;
reconsider i = (multrealpfunc A) . (a,g) as Element of PFuncs (A,REAL) ;
set j = (addpfunc A) . (f,g);
reconsider k = (multrealpfunc A) . (a,((addpfunc A) . (f,g))) as Element of PFuncs (A,REAL) ;
set l = (addpfunc A) . (h,i);
A1: ( dom h = dom f & dom i = dom g ) by Th9;
A2: dom ((addpfunc A) . (h,i)) = (dom h) /\ (dom i) by Th6;
A3: dom ((addpfunc A) . (f,g)) = (dom f) /\ (dom g) by Th6;
A4: now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_((addpfunc_A)_._(h,i))_holds_
((addpfunc_A)_._(h,i))_._x_=_k_._x
let x be Element of A; ::_thesis: ( x in dom ((addpfunc A) . (h,i)) implies ((addpfunc A) . (h,i)) . x = k . x )
A5: h . x = (a (#) f) . x by Def4;
assume A6: x in dom ((addpfunc A) . (h,i)) ; ::_thesis: ((addpfunc A) . (h,i)) . x = k . x
then A7: x in dom (f + g) by A1, A2, VALUED_1:def_1;
A8: i . x = (a (#) g) . x by Def4;
 x in dom i by A2, A6, XBOOLE_0:def_4;
then  x in dom g by Th9;
then  x in dom (a (#) g) by VALUED_1:def_5;
then A9: i . x = a * (g . x) by A8, VALUED_1:def_5;
 x in dom h by A2, A6, XBOOLE_0:def_4;
then  x in dom f by Th9;
then  x in dom (a (#) f) by VALUED_1:def_5;
then A10: h . x = a * (f . x) by A5, VALUED_1:def_5;
thus ((addpfunc A) . (h,i)) . x = (h . x) + (i . x) by A6, Th6
.= a * ((f . x) + (g . x)) by A10, A9
.= a * ((f + g) . x) by A7, VALUED_1:def_1
.= a * (((addpfunc A) . (f,g)) . x) by RFUNCT_3:def_4
.= k . x by A1, A3, A2, A6, Th9 ; ::_thesis: verum
end;
 dom k = dom ((addpfunc A) . (f,g)) by Th9;
hence  (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (a,g))) = (multrealpfunc A) . (a,((addpfunc A) . (f,g))) by A1, A3, A2, A4, PARTFUN1:5; ::_thesis: verum
end;

theorem :: LPSPACE1:20
for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))
proof
let A be non empty set ; ::_thesis: for f, g, h being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))
let f, g, h be Element of PFuncs (A,REAL); ::_thesis: (multpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))
set i = (multpfunc A) . (f,h);
set j = (multpfunc A) . (f,g);
set k = (addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)));
set l = (addpfunc A) . (g,h);
set m = (multpfunc A) . (f,((addpfunc A) . (g,h)));
A1: ((dom f) /\ (dom g)) /\ (dom h) = (dom f) /\ ((dom g) /\ (dom h)) by XBOOLE_1:16;
 ( dom ((multpfunc A) . (f,h)) = (dom f) /\ (dom h) & dom ((multpfunc A) . (f,g)) = (dom f) /\ (dom g) ) by Th7;
then  dom ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) = ((dom h) /\ (dom f)) /\ ((dom f) /\ (dom g)) by Th6;
then  dom ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) = (dom h) /\ ((dom f) /\ ((dom f) /\ (dom g))) by XBOOLE_1:16;
then A2: dom ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) = (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__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_((addpfunc_A)_._(((multpfunc_A)_._(f,g)),((multpfunc_A)_._(f,h))))_holds_
((addpfunc_A)_._(((multpfunc_A)_._(f,g)),((multpfunc_A)_._(f,h))))_._x_=_((multpfunc_A)_._(f,((addpfunc_A)_._(g,h))))_._x
let x be Element of A; ::_thesis: ( x in dom ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) implies ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = ((multpfunc A) . (f,((addpfunc A) . (g,h)))) . x )
assume A5: x in dom ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) ; ::_thesis: ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = ((multpfunc A) . (f,((addpfunc A) . (g,h)))) . x
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;
 ((multpfunc A) . (f,g)) . x = (f (#) g) . x by Def3;
then A8: ((multpfunc A) . (f,g)) . 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;
 ((multpfunc A) . (f,h)) . x = (f (#) h) . x by Def3;
then A10: ((multpfunc A) . (f,h)) . x = (f . x) * (h . x) by A9, VALUED_1:def_4;
 ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = (((multpfunc A) . (f,g)) . x) + (((multpfunc A) . (f,h)) . x) by A5, Th6;
then  ( ((addpfunc A) . (g,h)) . x = (g + h) . x & ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = (f . x) * ((g . x) + (h . x)) ) by A8, A10, RFUNCT_3:def_4;
then A11: ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = (f . x) * (((addpfunc A) . (g,h)) . x) by A7, VALUED_1:def_1;
 x in (dom f) /\ (dom ((addpfunc A) . (g,h))) by A2, A1, A5, Th6;
then A12: x in dom (f (#) ((addpfunc A) . (g,h))) by VALUED_1:def_4;
 ((multpfunc A) . (f,((addpfunc A) . (g,h)))) . x = (f (#) ((addpfunc A) . (g,h))) . x by Def3;
hence  ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = ((multpfunc A) . (f,((addpfunc A) . (g,h)))) . x by A12, A11, VALUED_1:def_4; ::_thesis: verum
end;
 ( dom ((multpfunc A) . (f,((addpfunc A) . (g,h)))) = (dom f) /\ (dom ((addpfunc A) . (g,h))) & dom ((addpfunc A) . (g,h)) = (dom g) /\ (dom h) ) by Th6, Th7;
hence  (multpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h))) by A2, A4, PARTFUN1:5, XBOOLE_1:16; ::_thesis: verum
end;

theorem :: LPSPACE1:21
for a being Real
for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (multpfunc A) . (((multrealpfunc A) . (a,f)),g) = (multrealpfunc A) . (a,((multpfunc A) . (f,g)))
proof
let a be Real; ::_thesis: for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (multpfunc A) . (((multrealpfunc A) . (a,f)),g) = (multrealpfunc A) . (a,((multpfunc A) . (f,g)))
let A be non empty set ; ::_thesis: for f, g being Element of PFuncs (A,REAL) holds (multpfunc A) . (((multrealpfunc A) . (a,f)),g) = (multrealpfunc A) . (a,((multpfunc A) . (f,g)))
let f, g be Element of PFuncs (A,REAL); ::_thesis: (multpfunc A) . (((multrealpfunc A) . (a,f)),g) = (multrealpfunc A) . (a,((multpfunc A) . (f,g)))
reconsider i = (multrealpfunc A) . (a,f) as Element of PFuncs (A,REAL) ;
set j = (multpfunc A) . (f,g);
set k = (multpfunc A) . (i,g);
reconsider l = (multrealpfunc A) . (a,((multpfunc A) . (f,g))) as Element of PFuncs (A,REAL) ;
A1: ( dom i = dom f & dom ((multpfunc A) . (i,g)) = (dom i) /\ (dom g) ) by Th7, Th9;
A2: dom ((multpfunc A) . (f,g)) = (dom f) /\ (dom g) by Th7;
A3: now__::_thesis:_for_x_being_Element_of_A_st_x_in_dom_((multpfunc_A)_._(i,g))_holds_
((multpfunc_A)_._(i,g))_._x_=_l_._x
let x be Element of A; ::_thesis: ( x in dom ((multpfunc A) . (i,g)) implies ((multpfunc A) . (i,g)) . x = l . x )
A4: ((multpfunc A) . (f,g)) . x = (f (#) g) . x by Def3;
assume A5: x in dom ((multpfunc A) . (i,g)) ; ::_thesis: ((multpfunc A) . (i,g)) . x = l . x
then  x in dom (f (#) g) by A1, VALUED_1:def_4;
then A6: ((multpfunc A) . (f,g)) . 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 (#) ((multpfunc A) . (f,g))) . x by Def4;
 x in dom (a (#) ((multpfunc A) . (f,g))) by A1, A2, A5, VALUED_1:def_5;
then A10: l . x = a * ((f . x) * (g . x)) by A6, A9, VALUED_1:def_5;
 ((multpfunc A) . (i,g)) . x = (i . x) * (g . x) by A5, Th7;
hence  ((multpfunc A) . (i,g)) . x = l . x by A8, A10; ::_thesis: verum
end;
 dom l = dom ((multpfunc A) . (f,g)) by Th9;
hence  (multpfunc A) . (((multrealpfunc A) . (a,f)),g) = (multrealpfunc A) . (a,((multpfunc A) . (f,g))) by A1, A2, A3, PARTFUN1:5; ::_thesis: verum
end;

definition
let A be non empty set ;
func RLSp_PFunct A ->  non empty RLSStruct  equals :: LPSPACE1:def 7
 RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #);
coherence
 RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #) is non empty RLSStruct ;
end;

:: deftheorem  defines RLSp_PFunct LPSPACE1:def_7_:_
 for A being non empty set holds RLSp_PFunct A = RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #);


registration
let A be non empty set ;
cluster RLSp_PFunct A ->  non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( RLSp_PFunct A is strict & RLSp_PFunct A is Abelian & RLSp_PFunct A is add-associative & RLSp_PFunct A is right_zeroed & RLSp_PFunct A is vector-distributive & RLSp_PFunct A is scalar-distributive & RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )
proof
set IT = RLSp_PFunct A;
thus  RLSp_PFunct A is strict ; ::_thesis: ( RLSp_PFunct A is Abelian & RLSp_PFunct A is add-associative & RLSp_PFunct A is right_zeroed & RLSp_PFunct A is vector-distributive & RLSp_PFunct A is scalar-distributive & RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )
thus  for u, v being VECTOR of (RLSp_PFunct A) holds u + v = v + u by Th10; :: according to RLVECT_1:def_2 ::_thesis: ( RLSp_PFunct A is add-associative & RLSp_PFunct A is right_zeroed & RLSp_PFunct A is vector-distributive & RLSp_PFunct A is scalar-distributive & RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )
thus  for u, v, w being VECTOR of (RLSp_PFunct A) holds (u + v) + w = u + (v + w) by Th11; :: according to RLVECT_1:def_3 ::_thesis: ( RLSp_PFunct A is right_zeroed & RLSp_PFunct A is vector-distributive & RLSp_PFunct A is scalar-distributive & RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )
thus  for u being VECTOR of (RLSp_PFunct A) holds u + (0. (RLSp_PFunct A)) = u :: according to RLVECT_1:def_4 ::_thesis: ( RLSp_PFunct A is vector-distributive & RLSp_PFunct A is scalar-distributive & RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )
proof
let u be VECTOR of (RLSp_PFunct A); ::_thesis: u + (0. (RLSp_PFunct A)) = u
reconsider u9 = u as Element of PFuncs (A,REAL) ;
thus u + (0. (RLSp_PFunct A)) = (addpfunc A) . ((RealPFuncZero A),u9) by Th10
.= u by Th15 ; ::_thesis: verum
end;
thus  for a being real number
for u, v being VECTOR of (RLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v) :: according to RLVECT_1:def_5 ::_thesis: ( RLSp_PFunct A is scalar-distributive & RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )
proof
let a be real number ; ::_thesis: for u, v being VECTOR of (RLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v)
reconsider a = a as Real by XREAL_0:def_1;
 for u, v being VECTOR of (RLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v) by Lm1;
hence  for u, v being VECTOR of (RLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v) ; ::_thesis: verum
end;
thus  for a, b being real number
for v being VECTOR of (RLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )
proof
let a, b be real number ; ::_thesis: for v being VECTOR of (RLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
 for v being VECTOR of (RLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v) by Th19;
hence  for v being VECTOR of (RLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum
end;
thus  for a, b being real number
for v being VECTOR of (RLSp_PFunct A) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: RLSp_PFunct A is scalar-unital
proof
let a, b be real number ; ::_thesis: for v being VECTOR of (RLSp_PFunct A) holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
 for v being VECTOR of (RLSp_PFunct A) holds (a * b) * v = a * (b * v) by Th18;
hence  for v being VECTOR of (RLSp_PFunct A) holds (a * b) * v = a * (b * v) ; ::_thesis: verum
end;
let v be VECTOR of (RLSp_PFunct A); :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v
thus  1 * v = v by Th17; ::_thesis: verum
end;
end;

begin


theorem Th22: :: LPSPACE1:22
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex E being Element of S st E = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex E being Element of S st E = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex E being Element of S st E = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL st ex E being Element of S st E = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let f be PartFunc of X,ExtREAL; ::_thesis: ( ex E being Element of S st E = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) implies ( f is_integrable_on M & Integral (M,f) = 0 ) )
given E being Element of S such that A1: E = dom f ; ::_thesis: ( ex x being Element of X st
( x in dom f & not 0 = f . x ) or ( f is_integrable_on M & Integral (M,f) = 0 ) )
assume A2: for x being Element of X st x in dom f holds
0 = f . x ; ::_thesis: ( f is_integrable_on M & Integral (M,f) = 0 )
then A3: for x being set st x in dom f holds
f . x = 0 ;
then A4: f is_simple_func_in S by A1, MESFUNC6:2;
then A5: integral+ (M,f) = 0 by A1, A2, MESFUNC2:34, MESFUNC5:87;
A6: dom (max+ f) = dom f by MESFUNC2:def_2;
A7: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_f_holds_
f_._x_=_(max+_f)_._x
let x be Element of X; ::_thesis: ( x in dom f implies f . x = (max+ f) . x )
assume A8: x in dom f ; ::_thesis: f . x = (max+ f) . x
hence f . x = max (0,0) by A2
.= max ((f . x),0) by A2, A8
.= (max+ f) . x by A6, A8, MESFUNC2:def_2 ;
::_thesis: verum
end;
A9: f is_measurable_on E by A1, A3, MESFUNC2:34, MESFUNC6:2;
A10: f is nonnegative
proof
let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( not y in rng f or 0. <= y )
assume  y in rng f ; ::_thesis: 0. <= y
then  ex x1 being set st
( x1 in dom f & y = f . x1 ) by FUNCT_1:def_3;
hence  y >= 0 by A2; ::_thesis: verum
end;
then  0. = Integral (M,f) by A1, A4, A5, MESFUNC2:34, MESFUNC5:88
.= (integral+ (M,f)) - (integral+ (M,(max- f))) by A6, A7, PARTFUN1:5
.= 0. + (- (integral+ (M,(max- f)))) by A1, A2, A4, MESFUNC2:34, MESFUNC5:87
.= - (integral+ (M,(max- f))) by XXREAL_3:4 ;
then A11: - (- (integral+ (M,(max- f)))) = - 0 ;
 integral+ (M,(max+ f)) < +infty by A6, A7, A5, PARTFUN1:5;
hence  f is_integrable_on M by A1, A9, A11, MESFUNC5:def_17; ::_thesis: Integral (M,f) = 0
thus  Integral (M,f) = 0 by A1, A9, A5, A10, MESFUNC5:88; ::_thesis: verum
end;

definition
let X be non empty set ;
let r be Real;
:: original: -->
redefine funcX --> r ->  PartFunc of X,REAL;
coherence
 X --> r is PartFunc of X,REAL
proof
thus  X --> r is PartFunc of X,REAL ; ::_thesis: verum
end;
end;

Lm2:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st X = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st X = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st X = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st X = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let f be PartFunc of X,REAL; ::_thesis: ( X = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) implies ( f is_integrable_on M & Integral (M,f) = 0 ) )
A1: X is Element of S by MEASURE1:7;
assume A2: ( X = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) ) ; ::_thesis: ( f is_integrable_on M & Integral (M,f) = 0 )
then  R_EAL f is_integrable_on M by A1, Th22;
hence  ( f is_integrable_on M & Integral (M,f) = 0 ) by A2, A1, Th22, MESFUNC6:def_4; ::_thesis: verum
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func L1_Functions M ->  non empty Subset of (RLSp_PFunct X) equals :: LPSPACE1:def 8
 {  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M )  }  ;
correctness
coherence
{  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M )  }  is non empty Subset of (RLSp_PFunct X);
proof
reconsider ND = {} as Element of S by MEASURE1:34;
set g = X --> 0;
set I =  {  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M )  }  ;
A1:  {  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M )  }  c= PFuncs (X,REAL)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M )  }  or x in PFuncs (X,REAL) )
assume  x in  {  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M )  }  ; ::_thesis: x in PFuncs (X,REAL)
then  ex f being PartFunc of X,REAL st
( x = f & ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) ) ;
hence  x in PFuncs (X,REAL) by PARTFUN1:45; ::_thesis: verum
end;
A2: dom (X --> 0) = ND ` by FUNCOP_1:13;
 for x being Element of X st x in dom (X --> 0) holds
(X --> 0) . x = 0 by FUNCOP_1:7;
then  ( M . ND = 0 & X --> 0 is_integrable_on M ) by A2, Lm2, VALUED_0:def_19;
then  X --> 0 in  {  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M )  }  by A2;
hence   {  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M )  }  is non empty Subset of (RLSp_PFunct X) by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines L1_Functions LPSPACE1:def_8_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L1_Functions M =  {  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M )  }  ;

Lm3:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S holds
( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S holds
( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M )
let M be sigma_Measure of S; ::_thesis: ( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M )
reconsider g = X --> 0 as Function of X,REAL by FUNCOP_1:46;
reconsider ND = {} as Element of S by MEASURE1:34;
A1: dom g = ND ` by FUNCT_2:def_1;
 for x being 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  ( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M ) by A1; ::_thesis: verum
end;

Lm4:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S st M . E1 = 0 & M . E2 = 0 holds
M . (E1 \/ E2) = 0
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S st M . E1 = 0 & M . E2 = 0 holds
M . (E1 \/ E2) = 0
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E1, E2 being Element of S st M . E1 = 0 & M . E2 = 0 holds
M . (E1 \/ E2) = 0
let M be sigma_Measure of S; ::_thesis: for E1, E2 being Element of S st M . E1 = 0 & M . E2 = 0 holds
M . (E1 \/ E2) = 0
let E1, E2 be Element of S; ::_thesis: ( M . E1 = 0 & M . E2 = 0 implies M . (E1 \/ E2) = 0 )
assume  ( M . E1 = 0 & M . E2 = 0 ) ; ::_thesis: M . (E1 \/ E2) = 0
then  ( E1 is measure_zero of M & E2 is measure_zero of M ) by MEASURE1:def_7;
then  E1 \/ E2 is measure_zero of M by MEASURE1:37;
hence  M . (E1 \/ E2) = 0 by MEASURE1:def_7; ::_thesis: verum
end;

theorem Th23: :: LPSPACE1:23
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
f + g in L1_Functions M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
f + g in L1_Functions M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
f + g in L1_Functions M
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
f + g in L1_Functions M
let f, g be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M & g in L1_Functions M implies f + g in L1_Functions M )
set W = L1_Functions M;
assume that
A1: f in L1_Functions M and
A2: g in L1_Functions M ; ::_thesis: f + g in L1_Functions M
 ex f1 being PartFunc of X,REAL st
( f1 = f & ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) ) by A1;
then consider NDv being Element of S such that
A3: M . NDv = 0 and
A4: dom f = NDv ` and
A5: f is_integrable_on M ;
 ex g1 being PartFunc of X,REAL st
( g1 = g & ex ND being Element of S st
( M . ND = 0 & dom g1 = ND ` & g1 is_integrable_on M ) ) by A2;
then consider NDu being Element of S such that
A6: M . NDu = 0 and
A7: dom g = NDu ` and
A8: g is_integrable_on M ;
A9: dom (f + g) = (NDv `) /\ (NDu `) by A4, A7, VALUED_1:def_1
.= (NDv \/ NDu) ` by XBOOLE_1:53 ;
 ( M . (NDv \/ NDu) = 0 & f + g is_integrable_on M ) by A3, A5, A6, A8, Lm4, MESFUNC6:100;
hence  f + g in L1_Functions M by A9; ::_thesis: verum
end;

theorem Th24: :: LPSPACE1:24
for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M holds
a (#) f in L1_Functions M
proof
let a be Real; ::_thesis: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M holds
a (#) f in L1_Functions M
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M holds
a (#) f in L1_Functions M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M holds
a (#) f in L1_Functions M
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st f in L1_Functions M holds
a (#) f in L1_Functions M
let f be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M implies a (#) f in L1_Functions M )
set W = L1_Functions M;
assume  f in L1_Functions M ; ::_thesis: a (#) f in L1_Functions M
then  ex f1 being PartFunc of X,REAL st
( f1 = f & ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) ) ;
then consider ND being Element of S such that
A1: M . ND = 0 and
A2: ( dom f = ND ` & f is_integrable_on M ) ;
 ( dom (a (#) f) = ND ` & a (#) f is_integrable_on M ) by A2, MESFUNC6:102, VALUED_1:def_5;
hence  a (#) f in L1_Functions M by A1; ::_thesis: verum
end;

Lm5:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( L1_Functions M is add-closed & L1_Functions M is multi-closed )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S holds
( L1_Functions M is add-closed & L1_Functions M is multi-closed )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S holds
( L1_Functions M is add-closed & L1_Functions M is multi-closed )
let M be sigma_Measure of S; ::_thesis: ( L1_Functions M is add-closed & L1_Functions M is multi-closed )
set W = L1_Functions M;
now__::_thesis:_for_v,_u_being_Element_of_(RLSp_PFunct_X)_st_v_in_L1_Functions_M_&_u_in_L1_Functions_M_holds_
v_+_u_in_L1_Functions_M
let v, u be Element of (RLSp_PFunct X); ::_thesis: ( v in L1_Functions M & u in L1_Functions M implies v + u in L1_Functions M )
assume that
A1: v in L1_Functions M and
A2: u in L1_Functions M ; ::_thesis: v + u in L1_Functions M
reconsider h = v + u as Element of PFuncs (X,REAL) ;
consider v1 being PartFunc of X,REAL such that
A3: v1 = v and
 ex ND being Element of S st
( M . ND = 0 & dom v1 = ND ` & v1 is_integrable_on M ) by A1;
consider u1 being PartFunc of X,REAL such that
A4: u1 = u and
 ex ND being 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 being set st x in dom h holds
h . x = (v1 . x) + (u1 . x) ) ) by A3, A4, Th6;
then  v + u = v1 + u1 by VALUED_1:def_1;
hence  v + u in L1_Functions M by A1, A2, A3, A4, Th23; ::_thesis: verum
end;
hence  L1_Functions M is add-closed by IDEAL_1:def_1; ::_thesis: L1_Functions M is multi-closed
now__::_thesis:_for_a_being_Real
for_u_being_VECTOR_of_(RLSp_PFunct_X)_st_u_in_L1_Functions_M_holds_
a_*_u_in_L1_Functions_M
let a be Real; ::_thesis: for u being VECTOR of (RLSp_PFunct X) st u in L1_Functions M holds
a * u in L1_Functions M
let u be VECTOR of (RLSp_PFunct X); ::_thesis: ( u in L1_Functions M implies a * u in L1_Functions M )
assume A5: u in L1_Functions M ; ::_thesis: a * u in L1_Functions M
consider u1 being PartFunc of X,REAL such that
A6: u1 = u and
 ex ND being Element of S st
( M . ND = 0 & dom u1 = ND ` & u1 is_integrable_on M ) by A5;
reconsider h = a * u as Element of PFuncs (X,REAL) ;
A7: dom h = dom u1 by A6, Th9;
then  for x being set st x in dom h holds
h . x = a * (u1 . x) by A6, Th9;
then  a * u = a (#) u1 by A7, VALUED_1:def_5;
hence  a * u in L1_Functions M by A5, A6, Th24; ::_thesis: verum
end;
hence  L1_Functions M is multi-closed by Def1; ::_thesis: verum
end;

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster L1_Functions M ->  non empty add-closed multi-closed ;
coherence
 ( L1_Functions M is multi-closed & L1_Functions M is add-closed ) by Lm5;
end;

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

:: deftheorem  defines RLSp_L1Funct LPSPACE1:def_9_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds RLSp_L1Funct M = RLSStruct(# (L1_Functions M),(In ((0. (RLSp_PFunct X)),(L1_Functions M))),(add| ((L1_Functions M),(RLSp_PFunct X))),(Mult_ (L1_Functions M)) #);

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster RLSp_L1Funct M ->  non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( RLSp_L1Funct M is strict & RLSp_L1Funct M is Abelian & RLSp_L1Funct M is add-associative & RLSp_L1Funct M is right_zeroed & RLSp_L1Funct M is vector-distributive & RLSp_L1Funct M is scalar-distributive & RLSp_L1Funct M is scalar-associative & RLSp_L1Funct M is scalar-unital )
proof
 0. (RLSp_PFunct X) in L1_Functions M by Lm3;
hence  ( RLSp_L1Funct M is strict & RLSp_L1Funct M is Abelian & RLSp_L1Funct M is add-associative & RLSp_L1Funct M is right_zeroed & RLSp_L1Funct M is vector-distributive & RLSp_L1Funct M is scalar-distributive & RLSp_L1Funct M is scalar-associative & RLSp_L1Funct M is scalar-unital ) by Th3; ::_thesis: verum
end;
end;

begin


theorem Th25: :: LPSPACE1:25
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for v, u being VECTOR of (RLSp_L1Funct M) st f = v & g = u holds
f + g = v + u
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for v, u being VECTOR of (RLSp_L1Funct M) st f = v & g = u holds
f + g = v + u
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for v, u being VECTOR of (RLSp_L1Funct M) st f = v & g = u holds
f + g = v + u
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL
for v, u being VECTOR of (RLSp_L1Funct M) st f = v & g = u holds
f + g = v + u
let f, g be PartFunc of X,REAL; ::_thesis: for v, u being VECTOR of (RLSp_L1Funct M) st f = v & g = u holds
f + g = v + u
let v, u be VECTOR of (RLSp_L1Funct M); ::_thesis: ( f = v & g = u implies f + g = v + u )
reconsider v2 = v as VECTOR of (RLSp_PFunct X) by TARSKI:def_3;
reconsider u2 = u as VECTOR of (RLSp_PFunct X) by TARSKI:def_3;
reconsider h = v2 + u2 as Element of PFuncs (X,REAL) ;
reconsider v3 = v2 as Element of PFuncs (X,REAL) ;
reconsider u3 = u2 as Element of PFuncs (X,REAL) ;
A1: dom h = (dom v3) /\ (dom u3) by Th6;
assume A2: ( f = v & g = u ) ; ::_thesis: f + g = v + u
then  for x being set st x in dom h holds
h . x = (f . x) + (g . x) by Th6;
then  h = f + g by A2, A1, VALUED_1:def_1;
hence  f + g = v + u by Th4; ::_thesis: verum
end;

theorem Th26: :: LPSPACE1:26
for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
a (#) f = a * u
proof
let a be Real; ::_thesis: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
a (#) f = a * u
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
a (#) f = a * u
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
a (#) f = a * u
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
a (#) f = a * u
let f be PartFunc of X,REAL; ::_thesis: for u being VECTOR of (RLSp_L1Funct M) st f = u holds
a (#) f = a * u
let u be VECTOR of (RLSp_L1Funct M); ::_thesis: ( f = u implies a (#) f = a * u )
reconsider u2 = u as VECTOR of (RLSp_PFunct X) by TARSKI:def_3;
reconsider h = a * u2 as Element of PFuncs (X,REAL) ;
assume A1: f = u ; ::_thesis: a (#) f = a * u
then A2: dom h = dom f by Th9;
then  for x being set st x in dom h holds
h . x = a * (f . x) by A1, Th9;
then  h = a (#) f by A2, VALUED_1:def_5;
hence  a (#) f = a * u by Th5; ::_thesis: verum
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f, g be PartFunc of X,REAL;
predf a.e.= g,M means :Def10: :: LPSPACE1:def 10
 ex E being Element of S st
( M . E = 0 & f | (E `) = g | (E `) );
end;

:: deftheorem Def10 defines a.e.= LPSPACE1:def_10_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL holds
( f a.e.= g,M iff ex E being Element of S st
( M . E = 0 & f | (E `) = g | (E `) ) );

theorem Th27: :: LPSPACE1:27
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
( u + ((- 1) * u) = (X --> 0) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in L1_Functions M & g in L1_Functions M & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
( u + ((- 1) * u) = (X --> 0) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in L1_Functions M & g in L1_Functions M & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
( u + ((- 1) * u) = (X --> 0) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in L1_Functions M & g in L1_Functions M & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
( u + ((- 1) * u) = (X --> 0) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in L1_Functions M & g in L1_Functions M & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
let f be PartFunc of X,REAL; ::_thesis: for u being VECTOR of (RLSp_L1Funct M) st f = u holds
( u + ((- 1) * u) = (X --> 0) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in L1_Functions M & g in L1_Functions M & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
let u be VECTOR of (RLSp_L1Funct M); ::_thesis: ( f = u implies ( u + ((- 1) * u) = (X --> 0) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in L1_Functions M & g in L1_Functions M & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) ) )
reconsider u2 = u as VECTOR of (RLSp_PFunct X) by TARSKI:def_3;
reconsider h = u2 + ((- 1) * u2) as Element of PFuncs (X,REAL) ;
set g = X --> 0;
 u + ((- 1) * u) in L1_Functions M ;
then consider v being PartFunc of X,REAL such that
A1: v = u + ((- 1) * u) and
 ex ND being Element of S st
( M . ND = 0 & dom v = ND ` & v is_integrable_on M ) ;
assume A2: f = u ; ::_thesis: ( u + ((- 1) * u) = (X --> 0) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in L1_Functions M & g in L1_Functions M & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )
then A3: h = (RealPFuncZero X) | (dom f) by Th16;
 u in L1_Functions M ;
then  ex uu1 being PartFunc of X,REAL st
( uu1 = u & ex ND being Element of S st
( M . ND = 0 & dom uu1 = ND ` & uu1 is_integrable_on M ) ) ;
then consider ND being Element of S such that
A4: M . ND = 0 and
A5: dom f = ND ` and
 f is_integrable_on M by A2;
A6: (- 1) * u2 = (- 1) * u by Th5;
hence  u + ((- 1) * u) = (X --> 0) | (dom f) by A3, Th4; ::_thesis: ex v, g being PartFunc of X,REAL st
( v in L1_Functions M & g in L1_Functions M & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M )
 v | (ND `) = ((X --> 0) | (ND `)) | (ND `) by A3, A6, A1, A5, Th4;
then  v | (ND `) = (X --> 0) | (ND `) by FUNCT_1:51;
then A7: v a.e.= X --> 0,M by A4, Def10;
 X --> 0 in L1_Functions M by Lm3;
hence  ex v, g being PartFunc of X,REAL st
( v in L1_Functions M & g in L1_Functions M & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) by A1, A7; ::_thesis: verum
end;

theorem Th28: :: LPSPACE1:28
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL holds f a.e.= f,M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL holds f a.e.= f,M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL holds f a.e.= f,M
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL holds f a.e.= f,M
let f be PartFunc of X,REAL; ::_thesis: f a.e.= f,M
 {} is Element of S by PROB_1:4;
then consider E being Element of S such that
A1: E = {} ;
A2: f | (E `) = f | (E `) ;
 M . E = 0 by A1, VALUED_0:def_19;
hence  f a.e.= f,M by A2, Def10; ::_thesis: verum
end;

theorem Th29: :: LPSPACE1:29
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
g a.e.= f,M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
g a.e.= f,M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
g a.e.= f,M
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f a.e.= g,M holds
g a.e.= f,M
let f, g be PartFunc of X,REAL; ::_thesis: ( f a.e.= g,M implies g a.e.= f,M )
assume  f a.e.= g,M ; ::_thesis: g a.e.= f,M
then  ex E being Element of S st
( M . E = 0 & f | (E `) = g | (E `) ) by Def10;
hence  g a.e.= f,M by Def10; ::_thesis: verum
end;

theorem Th30: :: LPSPACE1:30
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g, h being PartFunc of X,REAL st f a.e.= g,M & g a.e.= h,M holds
f a.e.= h,M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g, h being PartFunc of X,REAL st f a.e.= g,M & g a.e.= h,M holds
f a.e.= h,M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g, h being PartFunc of X,REAL st f a.e.= g,M & g a.e.= h,M holds
f a.e.= h,M
let M be sigma_Measure of S; ::_thesis: for f, g, h being PartFunc of X,REAL st f a.e.= g,M & g a.e.= h,M holds
f a.e.= h,M
let f, g, h be PartFunc of X,REAL; ::_thesis: ( f a.e.= g,M & g a.e.= h,M implies f a.e.= h,M )
assume that
A1: f a.e.= g,M and
A2: g a.e.= h,M ; ::_thesis: f a.e.= h,M
consider EQ1 being Element of S such that
A3: M . EQ1 = 0 and
A4: f | (EQ1 `) = g | (EQ1 `) by A1, Def10;
consider EQ2 being Element of S such that
A5: M . EQ2 = 0 and
A6: g | (EQ2 `) = h | (EQ2 `) by A2, Def10;
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  f a.e.= h,M by A7, Def10; ::_thesis: verum
end;

theorem Th31: :: LPSPACE1:31
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, f1, g, g1 being PartFunc of X,REAL st f a.e.= f1,M & g a.e.= g1,M holds
f + g a.e.= f1 + g1,M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, f1, g, g1 being PartFunc of X,REAL st f a.e.= f1,M & g a.e.= g1,M holds
f + g a.e.= f1 + g1,M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, f1, g, g1 being PartFunc of X,REAL st f a.e.= f1,M & g a.e.= g1,M holds
f + g a.e.= f1 + g1,M
let M be sigma_Measure of S; ::_thesis: for f, f1, g, g1 being PartFunc of X,REAL st f a.e.= f1,M & g a.e.= g1,M holds
f + g a.e.= f1 + g1,M
let f, f1, g, g1 be PartFunc of X,REAL; ::_thesis: ( f a.e.= f1,M & g a.e.= g1,M implies f + g a.e.= f1 + g1,M )
assume that
A1: f a.e.= f1,M and
A2: g a.e.= g1,M ; ::_thesis: f + g a.e.= f1 + g1,M
consider EQ1 being Element of S such that
A3: M . EQ1 = 0 and
A4: f | (EQ1 `) = f1 | (EQ1 `) by A1, Def10;
consider EQ2 being Element of S such that
A5: M . EQ2 = 0 and
A6: g | (EQ2 `) = g1 | (EQ2 `) by A2, Def10;
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  f + g a.e.= f1 + g1,M by A10, Def10; ::_thesis: verum
end;

theorem Th32: :: LPSPACE1:32
for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M
proof
let a be Real; ::_thesis: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M
let f, g be PartFunc of X,REAL; ::_thesis: ( f a.e.= g,M implies a (#) f a.e.= a (#) g,M )
assume  f a.e.= g,M ; ::_thesis: a (#) f a.e.= a (#) g,M
then consider E being Element of S such that
A1: M . E = 0 and
A2: f | (E `) = g | (E `) by Def10;
(a (#) f) | (E `) = a (#) (g | (E `)) by A2, RFUNCT_1:49
.= (a (#) g) | (E `) by RFUNCT_1:49 ;
hence  a (#) f a.e.= a (#) g,M by A1, Def10; ::_thesis: verum
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func AlmostZeroFunctions M ->  non empty Subset of (RLSp_L1Funct M) equals :: LPSPACE1:def 11
 {  f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0,M )  }  ;
coherence
  {  f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0,M )  }  is non empty Subset of (RLSp_L1Funct M)
proof
A1: now__::_thesis:_for_x_being_set_st_x_in__{__f_where_f_is_PartFunc_of_X,REAL_:_(_f_in_L1_Functions_M_&_f_a.e.=_X_-->_0,M_)__}__holds_
x_in_the_carrier_of_(RLSp_L1Funct_M)
let x be set ; ::_thesis: ( x in  {  f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0,M )  }  implies x in the carrier of (RLSp_L1Funct M) )
assume  x in  {  f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0,M )  }  ; ::_thesis: x in the carrier of (RLSp_L1Funct M)
then  ex f being PartFunc of X,REAL st
( x = f & f in L1_Functions M & f a.e.= X --> 0,M ) ;
hence  x in the carrier of (RLSp_L1Funct M) ; ::_thesis: verum
end;
 ( X --> 0 a.e.= X --> 0,M & X --> 0 in L1_Functions M ) by Lm3, Th28;
then  X --> 0 in  {  f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0,M )  }  ;
hence   {  f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0,M )  }  is non empty Subset of (RLSp_L1Funct M) by A1, TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines AlmostZeroFunctions LPSPACE1:def_11_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds AlmostZeroFunctions M =  {  f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0,M )  }  ;

theorem Th33: :: LPSPACE1:33
for a being Real
for X being non empty set holds
( (X --> 0) + (X --> 0) = X --> 0 & a (#) (X --> 0) = X --> 0 )
proof
let a be Real; ::_thesis: for X being non empty set holds
( (X --> 0) + (X --> 0) = X --> 0 & a (#) (X --> 0) = X --> 0 )
let X be non empty set ; ::_thesis: ( (X --> 0) + (X --> 0) = X --> 0 & a (#) (X --> 0) = X --> 0 )
set g1 = X --> 0;
set g2 = X --> 0;
A1: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(a_(#)_(X_-->_0))_holds_
(a_(#)_(X_-->_0))_._x_=_(X_-->_0)_._x
let x be Element of X; ::_thesis: ( x in dom (a (#) (X --> 0)) implies (a (#) (X --> 0)) . x = (X --> 0) . x )
assume  x in dom (a (#) (X --> 0)) ; ::_thesis: (a (#) (X --> 0)) . x = (X --> 0) . x
then  (a (#) (X --> 0)) . x = a * ((X --> 0) . x) by VALUED_1:def_5;
then  (a (#) (X --> 0)) . x = a * 0 by FUNCOP_1:7;
hence  (a (#) (X --> 0)) . x = (X --> 0) . x by FUNCOP_1:7; ::_thesis: verum
end;
A2: dom ((X --> 0) + (X --> 0)) = (dom (X --> 0)) /\ (dom (X --> 0)) by VALUED_1:def_1;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(X_-->_0)_holds_
((X_-->_0)_+_(X_-->_0))_._x_=_(X_-->_0)_._x
let x be Element of X; ::_thesis: ( x in dom (X --> 0) implies ((X --> 0) + (X --> 0)) . x = (X --> 0) . x )
assume  x in dom (X --> 0) ; ::_thesis: ((X --> 0) + (X --> 0)) . x = (X --> 0) . x
then  ((X --> 0) + (X --> 0)) . x = ((X --> 0) . x) + ((X --> 0) . x) by A2, VALUED_1:def_1;
then  ((X --> 0) + (X --> 0)) . x = 0 + ((X --> 0) . x) by FUNCOP_1:7;
hence  ((X --> 0) + (X --> 0)) . x = (X --> 0) . x ; ::_thesis: verum
end;
hence  (X --> 0) + (X --> 0) = X --> 0 by A2, PARTFUN1:5; ::_thesis: a (#) (X --> 0) = X --> 0
 dom (a (#) (X --> 0)) = dom (X --> 0) by VALUED_1:def_5;
hence  a (#) (X --> 0) = X --> 0 by A1, PARTFUN1:5; ::_thesis: verum
end;

Lm6:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S holds
( AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S holds
( AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed )
let M be sigma_Measure of S; ::_thesis: ( AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed )
set Z = AlmostZeroFunctions M;
set V = RLSp_L1Funct M;
now__::_thesis:_for_v,_u_being_VECTOR_of_(RLSp_L1Funct_M)_st_v_in_AlmostZeroFunctions_M_&_u_in_AlmostZeroFunctions_M_holds_
v_+_u_in_AlmostZeroFunctions_M
let v, u be VECTOR of (RLSp_L1Funct M); ::_thesis: ( v in AlmostZeroFunctions M & u in AlmostZeroFunctions M implies v + u in AlmostZeroFunctions M )
assume that
A1: v in AlmostZeroFunctions M and
A2: u in AlmostZeroFunctions M ; ::_thesis: v + u in AlmostZeroFunctions M
consider v1 being PartFunc of X,REAL such that
A3: v1 = v and
 v1 in L1_Functions M and
A4: v1 a.e.= X --> 0,M by A1;
consider u1 being PartFunc of X,REAL such that
A5: u1 = u and
 u1 in L1_Functions M and
A6: u1 a.e.= X --> 0,M by A2;
A7: v + u = v1 + u1 by A3, A5, Th25;
 (X --> 0) + (X --> 0) = X --> 0 by Th33;
then  v1 + u1 a.e.= X --> 0,M by A4, A6, Th31;
hence  v + u in AlmostZeroFunctions M by A7; ::_thesis: verum
end;
hence  AlmostZeroFunctions M is add-closed by IDEAL_1:def_1; ::_thesis: AlmostZeroFunctions M is multi-closed
now__::_thesis:_for_a_being_Real
for_u_being_VECTOR_of_(RLSp_L1Funct_M)_st_u_in_AlmostZeroFunctions_M_holds_
a_*_u_in_AlmostZeroFunctions_M
let a be Real; ::_thesis: for u being VECTOR of (RLSp_L1Funct M) st u in AlmostZeroFunctions M holds
a * u in AlmostZeroFunctions M
let u be VECTOR of (RLSp_L1Funct M); ::_thesis: ( u in AlmostZeroFunctions M implies a * u in AlmostZeroFunctions M )
assume  u in AlmostZeroFunctions M ; ::_thesis: a * u in AlmostZeroFunctions M
then consider u1 being PartFunc of X,REAL such that
A8: u1 = u and
 u1 in L1_Functions M and
A9: u1 a.e.= X --> 0,M ;
A10: a * u = a (#) u1 by A8, Th26;
 a (#) (X --> 0) = X --> 0 by Th33;
then  a (#) u1 a.e.= X --> 0,M by A9, Th32;
hence  a * u in AlmostZeroFunctions M by A10; ::_thesis: verum
end;
hence  AlmostZeroFunctions M is multi-closed by Def1; ::_thesis: verum
end;

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster AlmostZeroFunctions M ->  non empty add-closed multi-closed ;
coherence
 ( AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed ) by Lm6;
end;

theorem Th34: :: LPSPACE1:34
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( 0. (RLSp_L1Funct M) = X --> 0 & 0. (RLSp_L1Funct M) in AlmostZeroFunctions M )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S holds
( 0. (RLSp_L1Funct M) = X --> 0 & 0. (RLSp_L1Funct M) in AlmostZeroFunctions M )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S holds
( 0. (RLSp_L1Funct M) = X --> 0 & 0. (RLSp_L1Funct M) in AlmostZeroFunctions M )
let M be sigma_Measure of S; ::_thesis: ( 0. (RLSp_L1Funct M) = X --> 0 & 0. (RLSp_L1Funct M) in AlmostZeroFunctions M )
thus  0. (RLSp_L1Funct M) = X --> 0 by Lm3, FUNCT_7:def_1; ::_thesis: 0. (RLSp_L1Funct M) in AlmostZeroFunctions M
 ( X --> 0 a.e.= X --> 0,M & 0. (RLSp_L1Funct M) = 0. (RLSp_PFunct X) ) by Lm3, Th28, FUNCT_7:def_1;
hence  0. (RLSp_L1Funct M) in AlmostZeroFunctions M ; ::_thesis: verum
end;

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

:: deftheorem  defines RLSp_AlmostZeroFunct LPSPACE1:def_12_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds RLSp_AlmostZeroFunct M = RLSStruct(# (AlmostZeroFunctions M),(In ((0. (RLSp_L1Funct M)),(AlmostZeroFunctions M))),(add| ((AlmostZeroFunctions M),(RLSp_L1Funct M))),(Mult_ (AlmostZeroFunctions M)) #);

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster RLSp_L1Funct M ->  non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( RLSp_L1Funct M is strict & RLSp_L1Funct M is strict & RLSp_L1Funct M is Abelian & RLSp_L1Funct M is add-associative & RLSp_L1Funct M is right_zeroed & RLSp_L1Funct M is vector-distributive & RLSp_L1Funct M is scalar-distributive & RLSp_L1Funct M is scalar-associative & RLSp_L1Funct M is scalar-unital ) ;
end;


theorem :: LPSPACE1:35
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for v, u being VECTOR of (RLSp_AlmostZeroFunct M) st f = v & g = u holds
f + g = v + u
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for v, u being VECTOR of (RLSp_AlmostZeroFunct M) st f = v & g = u holds
f + g = v + u
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for v, u being VECTOR of (RLSp_AlmostZeroFunct M) st f = v & g = u holds
f + g = v + u
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL
for v, u being VECTOR of (RLSp_AlmostZeroFunct M) st f = v & g = u holds
f + g = v + u
let f, g be PartFunc of X,REAL; ::_thesis: for v, u being VECTOR of (RLSp_AlmostZeroFunct M) st f = v & g = u holds
f + g = v + u
let v, u be VECTOR of (RLSp_AlmostZeroFunct M); ::_thesis: ( f = v & g = u implies f + g = v + u )
assume A1: ( f = v & g = u ) ; ::_thesis: f + g = v + u
reconsider v2 = v, u2 = u as VECTOR of (RLSp_L1Funct M) by TARSKI:def_3;
thus v + u = v2 + u2 by Th4
.= f + g by A1, Th25 ; ::_thesis: verum
end;

theorem :: LPSPACE1:36
for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_AlmostZeroFunct M) st f = u holds
a (#) f = a * u
proof
let a be Real; ::_thesis: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_AlmostZeroFunct M) st f = u holds
a (#) f = a * u
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_AlmostZeroFunct M) st f = u holds
a (#) f = a * u
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_AlmostZeroFunct M) st f = u holds
a (#) f = a * u
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_AlmostZeroFunct M) st f = u holds
a (#) f = a * u
let f be PartFunc of X,REAL; ::_thesis: for u being VECTOR of (RLSp_AlmostZeroFunct M) st f = u holds
a (#) f = a * u
let u be VECTOR of (RLSp_AlmostZeroFunct M); ::_thesis: ( f = u implies a (#) f = a * u )
assume A1: f = u ; ::_thesis: a (#) f = a * u
reconsider u2 = u as VECTOR of (RLSp_L1Funct M) by TARSKI:def_3;
thus a * u = a * u2 by Th5
.= a (#) f by A1, Th26 ; ::_thesis: verum
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,REAL;
func a.e-eq-class (f,M) ->  Subset of (L1_Functions M) equals :: LPSPACE1:def 13
 {  g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M )  }  ;
correctness
coherence
{  g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M )  }  is Subset of (L1_Functions M);
proof
now__::_thesis:_for_x_being_set_st_x_in__{__g_where_g_is_PartFunc_of_X,REAL_:_(_g_in_L1_Functions_M_&_f_in_L1_Functions_M_&_f_a.e.=_g,M_)__}__holds_
x_in_L1_Functions_M
let x be set ; ::_thesis: ( x in  {  g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M )  }  implies x in L1_Functions M )
assume  x in  {  g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M )  }  ; ::_thesis: x in L1_Functions M
then  ex g being PartFunc of X,REAL st
( x = g & g in L1_Functions M & f in L1_Functions M & f a.e.= g,M ) ;
hence  x in L1_Functions M ; ::_thesis: verum
end;
hence   {  g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M )  }  is Subset of (L1_Functions M) by TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines a.e-eq-class LPSPACE1:def_13_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL holds a.e-eq-class (f,M) =  {  g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M )  }  ;

theorem Th37: :: LPSPACE1:37
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( g a.e.= f,M iff g in a.e-eq-class (f,M) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( g a.e.= f,M iff g in a.e-eq-class (f,M) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( g a.e.= f,M iff g in a.e-eq-class (f,M) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( g a.e.= f,M iff g in a.e-eq-class (f,M) )
let f, g be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M & g in L1_Functions M implies ( g a.e.= f,M iff g in a.e-eq-class (f,M) ) )
assume A1: ( f in L1_Functions M & g in L1_Functions M ) ; ::_thesis: ( g a.e.= f,M iff g in a.e-eq-class (f,M) )
hereby  ::_thesis: ( g in a.e-eq-class (f,M) implies g a.e.= f,M )
assume  g a.e.= f,M ; ::_thesis: g in a.e-eq-class (f,M)
then  f a.e.= g,M by Th29;
hence  g in a.e-eq-class (f,M) by A1; ::_thesis: verum
end;
hereby  ::_thesis: verum
assume  g in a.e-eq-class (f,M) ; ::_thesis: g a.e.= f,M
then  ex r being PartFunc of X,REAL st
( g = r & r in L1_Functions M & f in L1_Functions M & f a.e.= r,M ) ;
hence  g a.e.= f,M by Th29; ::_thesis: verum
end;
end;

theorem Th38: :: LPSPACE1:38
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M holds
f in a.e-eq-class (f,M)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M holds
f in a.e-eq-class (f,M)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M holds
f in a.e-eq-class (f,M)
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st f in L1_Functions M holds
f in a.e-eq-class (f,M)
let f be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M implies f in a.e-eq-class (f,M) )
hereby  ::_thesis: verum
assume A1: f in L1_Functions M ; ::_thesis: f in a.e-eq-class (f,M)
 f a.e.= f,M by Th28;
hence  f in a.e-eq-class (f,M) by A1; ::_thesis: verum
end;
end;

theorem Th39: :: LPSPACE1:39
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )
let f, g be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M & g in L1_Functions M implies ( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M ) )
assume that
A1: f in L1_Functions M and
A2: g in L1_Functions M ; ::_thesis: ( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )
hereby  ::_thesis: ( f a.e.= g,M implies a.e-eq-class (f,M) = a.e-eq-class (g,M) )
assume  a.e-eq-class (f,M) = a.e-eq-class (g,M) ; ::_thesis: f a.e.= g,M
then  f in  {  r where r is PartFunc of X,REAL : ( r in L1_Functions M & g in L1_Functions M & g a.e.= r,M )  }  by A1, Th38;
then  ex r being PartFunc of X,REAL st
( f = r & r in L1_Functions M & g in L1_Functions M & g a.e.= r,M ) ;
hence  f a.e.= g,M by Th29; ::_thesis: verum
end;
assume A3: f a.e.= g,M ; ::_thesis: a.e-eq-class (f,M) = a.e-eq-class (g,M)
now__::_thesis:_for_x_being_set_st_x_in_a.e-eq-class_(f,M)_holds_
x_in_a.e-eq-class_(g,M)
let x be set ; ::_thesis: ( x in a.e-eq-class (f,M) implies x in a.e-eq-class (g,M) )
assume  x in a.e-eq-class (f,M) ; ::_thesis: x in a.e-eq-class (g,M)
then consider r being PartFunc of X,REAL such that
A4: ( x = r & r in L1_Functions M ) and
 f in L1_Functions M and
A5: f a.e.= r,M ;
 g a.e.= f,M by A3, Th29;
then  g a.e.= r,M by A5, Th30;
hence  x in a.e-eq-class (g,M) by A2, A4; ::_thesis: verum
end;
then A6: a.e-eq-class (f,M) c= a.e-eq-class (g,M) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_a.e-eq-class_(g,M)_holds_
x_in_a.e-eq-class_(f,M)
let x be set ; ::_thesis: ( x in a.e-eq-class (g,M) implies x in a.e-eq-class (f,M) )
assume  x in a.e-eq-class (g,M) ; ::_thesis: x in a.e-eq-class (f,M)
then consider r being PartFunc of X,REAL such that
A7: ( x = r & r in L1_Functions M ) and
 g in L1_Functions M and
A8: g a.e.= r,M ;
 f a.e.= r,M by A3, A8, Th30;
hence  x in a.e-eq-class (f,M) by A1, A7; ::_thesis: verum
end;
then  a.e-eq-class (g,M) c= a.e-eq-class (f,M) by TARSKI:def_3;
hence  a.e-eq-class (f,M) = a.e-eq-class (g,M) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: LPSPACE1:40
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff g in a.e-eq-class (f,M) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff g in a.e-eq-class (f,M) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff g in a.e-eq-class (f,M) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff g in a.e-eq-class (f,M) )
let f, g be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M & g in L1_Functions M implies ( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff g in a.e-eq-class (f,M) ) )
assume A1: ( f in L1_Functions M & g in L1_Functions M ) ; ::_thesis: ( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff g in a.e-eq-class (f,M) )
then  ( g a.e.= f,M iff g in a.e-eq-class (f,M) ) by Th37;
hence  ( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff g in a.e-eq-class (f,M) ) by A1, Th39; ::_thesis: verum
end;

theorem Th41: :: LPSPACE1:41
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, f1, g, g1 being PartFunc of X,REAL st f in L1_Functions M & f1 in L1_Functions M & g in L1_Functions M & g1 in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (f1,M) & a.e-eq-class (g,M) = a.e-eq-class (g1,M) holds
a.e-eq-class ((f + g),M) = a.e-eq-class ((f1 + g1),M)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, f1, g, g1 being PartFunc of X,REAL st f in L1_Functions M & f1 in L1_Functions M & g in L1_Functions M & g1 in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (f1,M) & a.e-eq-class (g,M) = a.e-eq-class (g1,M) holds
a.e-eq-class ((f + g),M) = a.e-eq-class ((f1 + g1),M)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, f1, g, g1 being PartFunc of X,REAL st f in L1_Functions M & f1 in L1_Functions M & g in L1_Functions M & g1 in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (f1,M) & a.e-eq-class (g,M) = a.e-eq-class (g1,M) holds
a.e-eq-class ((f + g),M) = a.e-eq-class ((f1 + g1),M)
let M be sigma_Measure of S; ::_thesis: for f, f1, g, g1 being PartFunc of X,REAL st f in L1_Functions M & f1 in L1_Functions M & g in L1_Functions M & g1 in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (f1,M) & a.e-eq-class (g,M) = a.e-eq-class (g1,M) holds
a.e-eq-class ((f + g),M) = a.e-eq-class ((f1 + g1),M)
let f, f1, g, g1 be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M & f1 in L1_Functions M & g in L1_Functions M & g1 in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (f1,M) & a.e-eq-class (g,M) = a.e-eq-class (g1,M) implies a.e-eq-class ((f + g),M) = a.e-eq-class ((f1 + g1),M) )
assume that
A1: ( f in L1_Functions M & f1 in L1_Functions M & g in L1_Functions M & g1 in L1_Functions M ) and
A2: ( a.e-eq-class (f,M) = a.e-eq-class (f1,M) & a.e-eq-class (g,M) = a.e-eq-class (g1,M) ) ; ::_thesis: a.e-eq-class ((f + g),M) = a.e-eq-class ((f1 + g1),M)
 ( f a.e.= f1,M & g a.e.= g1,M ) by A1, A2, Th39;
then A3: f + g a.e.= f1 + g1,M by Th31;
 ( f + g in L1_Functions M & f1 + g1 in L1_Functions M ) by A1, Th23;
hence  a.e-eq-class ((f + g),M) = a.e-eq-class ((f1 + g1),M) by A3, Th39; ::_thesis: verum
end;

theorem Th42: :: LPSPACE1:42
for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (g,M) holds
a.e-eq-class ((a (#) f),M) = a.e-eq-class ((a (#) g),M)
proof
let a be Real; ::_thesis: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (g,M) holds
a.e-eq-class ((a (#) f),M) = a.e-eq-class ((a (#) g),M)
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (g,M) holds
a.e-eq-class ((a (#) f),M) = a.e-eq-class ((a (#) g),M)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (g,M) holds
a.e-eq-class ((a (#) f),M) = a.e-eq-class ((a (#) g),M)
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (g,M) holds
a.e-eq-class ((a (#) f),M) = a.e-eq-class ((a (#) g),M)
let f, g be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M & g in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (g,M) implies a.e-eq-class ((a (#) f),M) = a.e-eq-class ((a (#) g),M) )
assume that
A1: ( f in L1_Functions M & g in L1_Functions M ) and
A2: a.e-eq-class (f,M) = a.e-eq-class (g,M) ; ::_thesis: a.e-eq-class ((a (#) f),M) = a.e-eq-class ((a (#) g),M)
 f a.e.= g,M by A1, A2, Th39;
then A3: a (#) f a.e.= a (#) g,M by Th32;
 ( a (#) f in L1_Functions M & a (#) g in L1_Functions M ) by A1, Th24;
hence  a.e-eq-class ((a (#) f),M) = a.e-eq-class ((a (#) g),M) by A3, Th39; ::_thesis: verum
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func CosetSet M ->  non empty Subset-Family of (L1_Functions M) equals :: LPSPACE1:def 14
 {  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  ;
correctness
coherence
{  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  is non empty Subset-Family of (L1_Functions M);
proof
set C =  {  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  ;
A1:  {  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  c= bool (L1_Functions M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  or x in bool (L1_Functions M) )
assume  x in  {  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  ; ::_thesis: x in bool (L1_Functions M)
then  ex f being PartFunc of X,REAL st
( a.e-eq-class (f,M) = x & f in L1_Functions M ) ;
hence  x in bool (L1_Functions M) ; ::_thesis: verum
end;
 X --> 0 in L1_Functions M by Lm3;
then  a.e-eq-class ((X --> 0),M) in  {  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  ;
hence   {  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  is non empty Subset-Family of (L1_Functions M) by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines CosetSet LPSPACE1:def_14_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds CosetSet M =  {  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  ;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func addCoset M ->  BinOp of (CosetSet M) means :Def15: :: LPSPACE1:def 15
 for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
it . (A,B) = a.e-eq-class ((a + b),M);
existence
 ex b1 being BinOp of (CosetSet M) st
for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b1 . (A,B) = a.e-eq-class ((a + b),M)
proof
defpred S1[ set , set , set ] means  for a, b being PartFunc of X,REAL st a in $1 & b in $2 holds
$3 = a.e-eq-class ((a + b),M);
set C = CosetSet M;
A1: now__::_thesis:_for_A,_B_being_Element_of_CosetSet_M_ex_z_being_Element_of_CosetSet_M_st_S1[A,B,z]
let A, B be Element of CosetSet M; ::_thesis: ex z being Element of CosetSet M st S1[A,B,z]
 A in CosetSet M ;
then consider a being PartFunc of X,REAL such that
A2: A = a.e-eq-class (a,M) and
A3: a in L1_Functions M ;
 B in CosetSet M ;
then consider b being PartFunc of X,REAL such that
A4: B = a.e-eq-class (b,M) and
A5: b in L1_Functions M ;
set z = a.e-eq-class ((a + b),M);
A6: a + b in L1_Functions M by A3, A5, Th23;
then  a.e-eq-class ((a + b),M) in CosetSet M ;
then reconsider z = a.e-eq-class ((a + b),M) as Element of CosetSet M ;
take z = z; ::_thesis: S1[A,B,z]
now__::_thesis:_for_a1,_b1_being_PartFunc_of_X,REAL_st_a1_in_A_&_b1_in_B_holds_
z_=_a.e-eq-class_((a1_+_b1),M)
let a1, b1 be PartFunc of X,REAL; ::_thesis: ( a1 in A & b1 in B implies z = a.e-eq-class ((a1 + b1),M) )
assume A7: ( a1 in A & b1 in B ) ; ::_thesis: z = a.e-eq-class ((a1 + b1),M)
then  ( a1 a.e.= a,M & b1 a.e.= b,M ) by A2, A3, A4, A5, Th37;
then A8: a1 + b1 a.e.= a + b,M by Th31;
 a1 + b1 in L1_Functions M by A7, Th23;
hence  z = a.e-eq-class ((a1 + b1),M) by A6, A8, Th39; ::_thesis: verum
end;
hence  S1[A,B,z] ; ::_thesis: verum
end;
consider f being Function of [:(CosetSet M),(CosetSet M):],(CosetSet M) such that
A9: for A, B being Element of CosetSet M holds S1[A,B,f . (A,B)] from BINOP_1:sch_3(A1);
reconsider f = f as BinOp of (CosetSet M) ;
take  f ; ::_thesis: for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
f . (A,B) = a.e-eq-class ((a + b),M)
let A, B be Element of CosetSet M; ::_thesis: for a, b being PartFunc of X,REAL st a in A & b in B holds
f . (A,B) = a.e-eq-class ((a + b),M)
let a, b be PartFunc of X,REAL; ::_thesis: ( a in A & b in B implies f . (A,B) = a.e-eq-class ((a + b),M) )
assume  ( a in A & b in B ) ; ::_thesis: f . (A,B) = a.e-eq-class ((a + b),M)
hence  f . (A,B) = a.e-eq-class ((a + b),M) by A9; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (CosetSet M) st ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b1 . (A,B) = a.e-eq-class ((a + b),M) ) & ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b2 . (A,B) = a.e-eq-class ((a + b),M) ) holds
b1 = b2
proof
set C = CosetSet M;
let f1, f2 be BinOp of (CosetSet M); ::_thesis: ( ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
f1 . (A,B) = a.e-eq-class ((a + b),M) ) & ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
f2 . (A,B) = a.e-eq-class ((a + b),M) ) implies f1 = f2 )
assume that
A10: for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
f1 . (A,B) = a.e-eq-class ((a + b),M) and
A11: for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
f2 . (A,B) = a.e-eq-class ((a + b),M) ; ::_thesis: f1 = f2
now__::_thesis:_for_A,_B_being_Element_of_CosetSet_M_holds_f1_._(A,B)_=_f2_._(A,B)
let A, B be Element of CosetSet M; ::_thesis: f1 . (A,B) = f2 . (A,B)
 A in CosetSet M ;
then consider a1 being PartFunc of X,REAL such that
A12: ( A = a.e-eq-class (a1,M) & a1 in L1_Functions M ) ;
 B in CosetSet M ;
then consider b1 being PartFunc of X,REAL such that
A13: ( B = a.e-eq-class (b1,M) & b1 in L1_Functions M ) ;
A14: b1 in B by A13, Th38;
A15: a1 in A by A12, Th38;
then  f1 . (A,B) = a.e-eq-class ((a1 + b1),M) by A10, A14;
hence  f1 . (A,B) = f2 . (A,B) by A11, A15, A14; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines addCoset LPSPACE1:def_15_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being BinOp of (CosetSet M) holds
( b4 = addCoset M iff for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b4 . (A,B) = a.e-eq-class ((a + b),M) );

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func zeroCoset M ->  Element of CosetSet M means :Def16: :: LPSPACE1:def 16
 ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & it = a.e-eq-class (f,M) );
correctness
existence
ex b1 being Element of CosetSet M ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b1 = a.e-eq-class (f,M) );
uniqueness
for b1, b2 being Element of CosetSet M st ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b1 = a.e-eq-class (f,M) ) & ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b2 = a.e-eq-class (f,M) ) holds
b1 = b2;
proof
 X --> 0 in L1_Functions M by Lm3;
then  a.e-eq-class ((X --> 0),M) in CosetSet M ;
hence  ( ex b1 being Element of CosetSet M ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b1 = a.e-eq-class (f,M) ) & ( for b1, b2 being Element of CosetSet M st ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b1 = a.e-eq-class (f,M) ) & ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b2 = a.e-eq-class (f,M) ) holds
b1 = b2 ) ) by Lm3; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines zeroCoset LPSPACE1:def_16_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Element of CosetSet M holds
( b4 = zeroCoset M iff ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b4 = a.e-eq-class (f,M) ) );

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func lmultCoset M ->  Function of [:REAL,(CosetSet M):],(CosetSet M) means :Def17: :: LPSPACE1:def 17
 for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
it . (z,A) = a.e-eq-class ((z (#) f),M);
existence
 ex b1 being Function of [:REAL,(CosetSet M):],(CosetSet M) st
for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b1 . (z,A) = a.e-eq-class ((z (#) f),M)
proof
defpred S1[ Element of REAL , set , set ] means  for f being PartFunc of X,REAL st f in $2 holds
$3 = a.e-eq-class (($1 (#) f),M);
set C = CosetSet M;
A1: now__::_thesis:_for_z_being_Element_of_REAL_
for_A_being_Element_of_CosetSet_M_ex_c_being_Element_of_CosetSet_M_st_S1[z,A,c]
let z be Element of REAL ; ::_thesis: for A being Element of CosetSet M ex c being Element of CosetSet M st S1[z,A,c]
let A be Element of CosetSet M; ::_thesis: ex c being Element of CosetSet M st S1[z,A,c]
 A in CosetSet M ;
then consider a being PartFunc of X,REAL such that
A2: A = a.e-eq-class (a,M) and
A3: a in L1_Functions M ;
set c = a.e-eq-class ((z (#) a),M);
A4: z (#) a in L1_Functions M by A3, Th24;
then  a.e-eq-class ((z (#) a),M) in CosetSet M ;
then reconsider c = a.e-eq-class ((z (#) a),M) as Element of CosetSet M ;
take c = c; ::_thesis: S1[z,A,c]
now__::_thesis:_for_a1_being_PartFunc_of_X,REAL_st_a1_in_A_holds_
c_=_a.e-eq-class_((z_(#)_a1),M)
let a1 be PartFunc of X,REAL; ::_thesis: ( a1 in A implies c = a.e-eq-class ((z (#) a1),M) )
assume A5: a1 in A ; ::_thesis: c = a.e-eq-class ((z (#) a1),M)
then  a1 a.e.= a,M by A2, A3, Th37;
then A6: z (#) a1 a.e.= z (#) a,M by Th32;
 z (#) a1 in L1_Functions M by A5, Th24;
hence  c = a.e-eq-class ((z (#) a1),M) by A4, A6, Th39; ::_thesis: verum
end;
hence  S1[z,A,c] ; ::_thesis: verum
end;
consider f being Function of [:REAL,(CosetSet M):],(CosetSet M) such that
A7: for z being Element of REAL
for A being Element of CosetSet M holds S1[z,A,f . (z,A)] from BINOP_1:sch_3(A1);
take  f ; ::_thesis: for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
f . (z,A) = a.e-eq-class ((z (#) f),M)
let z be Element of REAL ; ::_thesis: for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
f . (z,A) = a.e-eq-class ((z (#) f),M)
let A be Element of CosetSet M; ::_thesis: for f being PartFunc of X,REAL st f in A holds
f . (z,A) = a.e-eq-class ((z (#) f),M)
let a be PartFunc of X,REAL; ::_thesis: ( a in A implies f . (z,A) = a.e-eq-class ((z (#) a),M) )
assume  a in A ; ::_thesis: f . (z,A) = a.e-eq-class ((z (#) a),M)
hence  f . (z,A) = a.e-eq-class ((z (#) a),M) by A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:REAL,(CosetSet M):],(CosetSet M) st ( for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b1 . (z,A) = a.e-eq-class ((z (#) f),M) ) & ( for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b2 . (z,A) = a.e-eq-class ((z (#) f),M) ) holds
b1 = b2
proof
set C = CosetSet M;
let f1, f2 be Function of [:REAL,(CosetSet M):],(CosetSet M); ::_thesis: ( ( for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
f1 . (z,A) = a.e-eq-class ((z (#) f),M) ) & ( for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
f2 . (z,A) = a.e-eq-class ((z (#) f),M) ) implies f1 = f2 )
assume that
A8: for z being Element of REAL
for A being Element of CosetSet M
for a being PartFunc of X,REAL st a in A holds
f1 . (z,A) = a.e-eq-class ((z (#) a),M) and
A9: for z being Element of REAL
for A being Element of CosetSet M
for a being PartFunc of X,REAL st a in A holds
f2 . (z,A) = a.e-eq-class ((z (#) a),M) ; ::_thesis: f1 = f2
now__::_thesis:_for_z_being_Element_of_REAL_
for_A_being_Element_of_CosetSet_M_holds_f1_._(z,A)_=_f2_._(z,A)
let z be Element of REAL ; ::_thesis: for A being Element of CosetSet M holds f1 . (z,A) = f2 . (z,A)
let A be Element of CosetSet M; ::_thesis: f1 . (z,A) = f2 . (z,A)
 A in CosetSet M ;
then consider a1 being PartFunc of X,REAL such that
A10: ( A = a.e-eq-class (a1,M) & a1 in L1_Functions M ) ;
thus f1 . (z,A) = a.e-eq-class ((z (#) a1),M) by A8, A10, Th38
.= f2 . (z,A) by A9, A10, Th38 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def17 defines lmultCoset LPSPACE1:def_17_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Function of [:REAL,(CosetSet M):],(CosetSet M) holds
( b4 = lmultCoset M iff for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b4 . (z,A) = a.e-eq-class ((z (#) f),M) );

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func Pre-L-Space M ->  non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct  means :Def18: :: LPSPACE1:def 18
( the carrier of it = CosetSet M & the addF of it = addCoset M & 0. it = zeroCoset M & the Mult of it = lmultCoset M );
existence
 ex b1 being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct st
( the carrier of b1 = CosetSet M & the addF of b1 = addCoset M & 0. b1 = zeroCoset M & the Mult of b1 = lmultCoset M )
proof
set C = CosetSet M;
set aC = addCoset M;
set zC = zeroCoset M;
set lC = lmultCoset M;
set A = RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #);
A1: RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) is Abelian
proof
let A1, A2 be Element of RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #); :: according to RLVECT_1:def_2 ::_thesis: A1 + A2 = A2 + A1
 A1 in CosetSet M ;
then consider a being PartFunc of X,REAL such that
A2: ( A1 = a.e-eq-class (a,M) & a in L1_Functions M ) ;
 A2 in CosetSet M ;
then consider b being PartFunc of X,REAL such that
A3: ( A2 = a.e-eq-class (b,M) & b in L1_Functions M ) ;
A4: b in A2 by A3, Th38;
A5: a in A1 by A2, Th38;
then  A1 + A2 = a.e-eq-class ((a + b),M) by A4, Def15;
hence  A1 + A2 = A2 + A1 by A5, A4, Def15; ::_thesis: verum
end;
A6: RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) is right_zeroed
proof
consider z being PartFunc of X,REAL such that
A7: z = X --> 0 and
A8: z in L1_Functions M and
A9: zeroCoset M = a.e-eq-class (z,M) by Def16;
A10: z in 0. RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) by A8, A9, Th38;
let A1 be Element of RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #); :: according to RLVECT_1:def_4 ::_thesis: A1 + (0. RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #)) = A1
 A1 in CosetSet M ;
then consider a being PartFunc of X,REAL such that
A11: A1 = a.e-eq-class (a,M) and
A12: a in L1_Functions M ;
reconsider a1 = a, z1 = z as VECTOR of (RLSp_L1Funct M) by A12, A8;
A13: a + z = a1 + z1 by Th25
.= a1 + (0. (RLSp_L1Funct M)) by A7, Th34
.= a by RLVECT_1:def_4 ;
 a in A1 by A11, A12, Th38;
hence  A1 + (0. RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #)) = A1 by A11, A10, A13, Def15; ::_thesis: verum
end;
A14: now__::_thesis:_for_x,_y_being_real_number_
for_A1,_A2_being_Element_of_RLSStruct(#_(CosetSet_M),(zeroCoset_M),(addCoset_M),(lmultCoset_M)_#)_holds_
(_x_*_(A1_+_A2)_=_(x_*_A1)_+_(x_*_A2)_&_(x_+_y)_*_A1_=_(x_*_A1)_+_(y_*_A1)_&_(x_*_y)_*_A1_=_x_*_(y_*_A1)_&_1_*_A1_=_A1_)
let x, y be real number ; ::_thesis: for A1, A2 being Element of RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) holds
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1 * A1 = A1 )
let A1, A2 be Element of RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #); ::_thesis: ( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1 * A1 = A1 )
reconsider x1 = x, y1 = y as Real by XREAL_0:def_1;
 A1 in CosetSet M ;
then consider a being PartFunc of X,REAL such that
A15: A1 = a.e-eq-class (a,M) and
A16: a in L1_Functions M ;
A17: a in A1 by A15, A16, Th38;
then  (lmultCoset M) . (x1,A1) = a.e-eq-class ((x (#) a),M) by Def17;
then A18: x (#) a in x * A1 by A16, Th24, Th38;
 A2 in CosetSet M ;
then consider b being PartFunc of X,REAL such that
A19: A2 = a.e-eq-class (b,M) and
A20: b in L1_Functions M ;
reconsider a1 = a, b1 = b as VECTOR of (RLSp_L1Funct M) by A16, A20;
A21: x (#) a = x1 * a1 by Th26;
A22: b in A2 by A19, A20, Th38;
then  (lmultCoset M) . (x1,A2) = a.e-eq-class ((x (#) b),M) by Def17;
then A23: x (#) b in x1 * A2 by A20, Th24, Th38;
 a + b = a1 + b1 by Th25;
then  x (#) (a + b) = x1 * (a1 + b1) by Th26;
then A24: x (#) (a + b) = (x * a1) + (x * b1) by RLVECT_1:def_5;
 x (#) b = x1 * b1 by Th26;
then A25: x (#) (a + b) = (x (#) a) + (x (#) b) by A21, A24, Th25;
 (addCoset M) . (A1,A2) = a.e-eq-class ((a + b),M) by A17, A22, Def15;
then  a + b in A1 + A2 by A16, A20, Th23, Th38;
then  x1 * (A1 + A2) = a.e-eq-class (((x (#) a) + (x (#) b)),M) by A25, Def17;
hence  x * (A1 + A2) = (x * A1) + (x * A2) by A18, A23, Def15; ::_thesis: ( (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & 1 * A1 = A1 )
A26: y (#) a = y1 * a1 by Th26;
 (lmultCoset M) . (y1,A1) = a.e-eq-class ((y (#) a),M) by A17, Def17;
then A27: y (#) a in y1 * A1 by A16, Th24, Th38;
(x + y) (#) a = (x1 + y1) * a1 by Th26
.= (x * a1) + (y * a1) by RLVECT_1:def_6
.= (x (#) a) + (y (#) a) by A26, A21, Th25 ;
then  (x1 + y1) * A1 = a.e-eq-class (((x (#) a) + (y (#) a)),M) by A17, Def17;
hence  (x + y) * A1 = (x * A1) + (y * A1) by A18, A27, Def15; ::_thesis: ( (x * y) * A1 = x * (y * A1) & 1 * A1 = A1 )
x (#) (y (#) a) = x * (y * a1) by A26, A21, Th26
.= (x1 * y1) * a1 by RLVECT_1:def_7
.= (x * y) (#) a by Th26 ;
then (x1 * y1) * A1 = a.e-eq-class ((x1 (#) (y1 (#) a)),M) by A17, Def17
.= x * (y * A1) by A27, Def17 ;
hence  (x * y) * A1 = x * (y * A1) ; ::_thesis: 1 * A1 = A1
1 (#) a = 1 * a1 by Th26
.= a by RLVECT_1:def_8 ;
hence  1 * A1 = A1 by A15, A17, Def17; ::_thesis: verum
end;
A28: RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) is right_complementable
proof
let A1 be Element of RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #); :: according to ALGSTR_0:def_16 ::_thesis: A1 is right_complementable
 A1 in CosetSet M ;
then consider a being PartFunc of X,REAL such that
A29: A1 = a.e-eq-class (a,M) and
A30: a in L1_Functions M ;
set A2 = a.e-eq-class (((- 1) (#) a),M);
A31: (- 1) (#) a in L1_Functions M by A30, Th24;
then  a.e-eq-class (((- 1) (#) a),M) in CosetSet M ;
then reconsider A2 = a.e-eq-class (((- 1) (#) a),M) as Element of RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) ;
A32: ( a in A1 & (- 1) (#) a in A2 ) by A29, A30, Th24, Th38;
reconsider a1 = a as VECTOR of (RLSp_L1Funct M) by A30;
take  A2 ; :: according to ALGSTR_0:def_11 ::_thesis: A1 + A2 = 0. RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #)
consider v, g being PartFunc of X,REAL such that
 v in L1_Functions M and
 g in L1_Functions M and
A33: v = a1 + ((- 1) * a1) and
A34: g = X --> 0 and
A35: v a.e.= g,M by Th27;
A36: ex z being PartFunc of X,REAL st
( z = X --> 0 & z in L1_Functions M & zeroCoset M = a.e-eq-class (z,M) ) by Def16;
A37: a + ((- 1) (#) a) in L1_Functions M by A30, A31, Th23;
 (- 1) (#) a = (- 1) * a1 by Th26;
then  a + ((- 1) (#) a) a.e.= g,M by A33, A35, Th25;
then  0. RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) = a.e-eq-class ((a + ((- 1) (#) a)),M) by A34, A37, A36, Th39;
hence  A1 + A2 = 0. RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) by A32, Def15; ::_thesis: verum
end;
 RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) is add-associative
proof
let A1, A2, A3 be Element of RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #); :: according to RLVECT_1:def_3 ::_thesis: (A1 + A2) + A3 = A1 + (A2 + A3)
 A1 in CosetSet M ;
then consider a being PartFunc of X,REAL such that
A38: A1 = a.e-eq-class (a,M) and
A39: a in L1_Functions M ;
 A2 in CosetSet M ;
then consider b being PartFunc of X,REAL such that
A40: A2 = a.e-eq-class (b,M) and
A41: b in L1_Functions M ;
 A3 in CosetSet M ;
then consider c being PartFunc of X,REAL such that
A42: A3 = a.e-eq-class (c,M) and
A43: c in L1_Functions M ;
A44: c in A3 by A42, A43, Th38;
A45: b in A2 by A40, A41, Th38;
then  (addCoset M) . (A2,A3) = a.e-eq-class ((b + c),M) by A44, Def15;
then A46: b + c in A2 + A3 by A41, A43, Th23, Th38;
reconsider a1 = a, b1 = b, c1 = c as VECTOR of (RLSp_L1Funct M) by A39, A41, A43;
 b + c = b1 + c1 by Th25;
then  a + (b + c) = a1 + (b1 + c1) by Th25;
then A47: a + (b + c) = (a1 + b1) + c1 by RLVECT_1:def_3;
 a + b = a1 + b1 by Th25;
then A48: a + (b + c) = (a + b) + c by A47, Th25;
A49: a in A1 by A38, A39, Th38;
then  (addCoset M) . (A1,A2) = a.e-eq-class ((a + b),M) by A45, Def15;
then  a + b in A1 + A2 by A39, A41, Th23, Th38;
then  (A1 + A2) + A3 = a.e-eq-class ((a + (b + c)),M) by A44, A48, Def15;
hence  (A1 + A2) + A3 = A1 + (A2 + A3) by A49, A46, Def15; ::_thesis: verum
end;
then reconsider A = RLSStruct(# (CosetSet M),(zeroCoset M),(addCoset M),(lmultCoset M) #) as non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct by A1, A6, A28, A14, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8;
take  A ; ::_thesis: ( the carrier of A = CosetSet M & the addF of A = addCoset M & 0. A = zeroCoset M & the Mult of A = lmultCoset M )
thus  ( the carrier of A = CosetSet M & the addF of A = addCoset M & 0. A = zeroCoset M & the Mult of A = lmultCoset M ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct st the carrier of b1 = CosetSet M & the addF of b1 = addCoset M & 0. b1 = zeroCoset M & the Mult of b1 = lmultCoset M & the carrier of b2 = CosetSet M & the addF of b2 = addCoset M & 0. b2 = zeroCoset M & the Mult of b2 = lmultCoset M holds
b1 = b2 ;
end;

:: deftheorem Def18 defines Pre-L-Space LPSPACE1:def_18_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct holds
( b4 = Pre-L-Space M iff ( the carrier of b4 = CosetSet M & the addF of b4 = addCoset M & 0. b4 = zeroCoset M & the Mult of b4 = lmultCoset M ) );

begin

theorem Th43: :: LPSPACE1:43
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
Integral (M,f) = Integral (M,g)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
Integral (M,f) = Integral (M,g)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
Integral (M,f) = Integral (M,g)
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
Integral (M,f) = Integral (M,g)
let f, g be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M & g in L1_Functions M & f a.e.= g,M implies Integral (M,f) = Integral (M,g) )
assume that
A1: f in L1_Functions M and
A2: g in L1_Functions M and
A3: f a.e.= g,M ; ::_thesis: Integral (M,f) = Integral (M,g)
consider EQ being Element of S such that
A4: M . EQ = 0 and
A5: f | (EQ `) = g | (EQ `) by A3, Def10;
A6: ex f1 being PartFunc of X,REAL st
( f = f1 & ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) ) by A1;
then consider NDf being Element of S such that
A7: M . NDf = 0 and
A8: dom f = NDf ` and
 f is_integrable_on M ;
A9: M . (EQ \/ NDf) = 0 by A7, A4, Lm4;
 R_EAL f is_integrable_on M by A6, MESFUNC6:def_4;
then consider E1 being Element of S such that
A10: E1 = dom (R_EAL f) and
A11: R_EAL f is_measurable_on E1 by MESFUNC5:def_17;
A12: f is_measurable_on E1 by A11, MESFUNC6:def_1;
A13: ex g1 being PartFunc of X,REAL st
( g = g1 & ex ND being Element of S st
( M . ND = 0 & dom g1 = ND ` & g1 is_integrable_on M ) ) by A2;
then consider NDg being Element of S such that
A14: M . NDg = 0 and
A15: dom g = NDg ` and
 g is_integrable_on M ;
A16: M . (EQ \/ NDg) = 0 by A14, A4, Lm4;
 R_EAL g is_integrable_on M by A13, MESFUNC6:def_4;
then consider E2 being Element of S such that
A17: E2 = dom (R_EAL g) and
A18: R_EAL g is_measurable_on E2 by MESFUNC5:def_17;
A19: g is_measurable_on E2 by A18, MESFUNC6:def_1;
A20: (EQ `) \ (NDf \/ NDg) = (EQ \/ (NDf \/ NDg)) ` by XBOOLE_1:41
.= (NDg \/ (EQ \/ NDf)) ` by XBOOLE_1:4
.= (NDg `) \ (EQ \/ NDf) by XBOOLE_1:41 ;
A21: (EQ `) \ (NDf \/ NDg) = (EQ \/ (NDf \/ NDg)) ` by XBOOLE_1:41
.= (NDf \/ (EQ \/ NDg)) ` by XBOOLE_1:4
.= (NDf `) \ (EQ \/ NDg) by XBOOLE_1:41 ;
A22: (EQ `) \ (NDf \/ NDg) c= EQ ` by XBOOLE_1:36;
then f | ((EQ `) \ (NDf \/ NDg)) = (g | (EQ `)) | ((EQ `) \ (NDf \/ NDg)) by A5, FUNCT_1:51
.= g | ((EQ `) \ (NDf \/ NDg)) by A22, FUNCT_1:51 ;
hence  Integral (M,f) = Integral (M,(g | ((NDg `) \ (EQ \/ NDf)))) by A8, A10, A12, A21, A20, A16, MESFUNC6:89
.= Integral (M,g) by A15, A17, A19, A9, MESFUNC6:89 ;
::_thesis: verum
end;

theorem Th44: :: LPSPACE1:44
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_integrable_on M holds
( Integral (M,f) in REAL & Integral (M,(abs f)) in REAL & abs f is_integrable_on M )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_integrable_on M holds
( Integral (M,f) in REAL & Integral (M,(abs f)) in REAL & abs f is_integrable_on M )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_integrable_on M holds
( Integral (M,f) in REAL & Integral (M,(abs f)) in REAL & abs f is_integrable_on M )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st f is_integrable_on M holds
( Integral (M,f) in REAL & Integral (M,(abs f)) in REAL & abs f is_integrable_on M )
let f be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M implies ( Integral (M,f) in REAL & Integral (M,(abs f)) in REAL & abs f is_integrable_on M ) )
assume A1: f is_integrable_on M ; ::_thesis: ( Integral (M,f) in REAL & Integral (M,(abs f)) in REAL & abs f is_integrable_on M )
then A2: ( -infty < Integral (M,f) & Integral (M,f) < +infty ) by MESFUNC6:90;
 R_EAL f is_integrable_on M by A1, MESFUNC6:def_4;
then consider A being Element of S such that
A3: A = dom (R_EAL f) and
A4: R_EAL f is_measurable_on A by MESFUNC5:def_17;
A5: f is_measurable_on A by A4, MESFUNC6:def_1;
then  abs f is_integrable_on M by A1, A3, MESFUNC6:94;
then  ( -infty < Integral (M,(abs f)) & Integral (M,(abs f)) < +infty ) by MESFUNC6:90;
hence  ( Integral (M,f) in REAL & Integral (M,(abs f)) in REAL & abs f is_integrable_on M ) by A1, A2, A3, A5, MESFUNC6:94, XXREAL_0:14; ::_thesis: verum
end;

theorem Th45: :: LPSPACE1:45
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) )
let f, g be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M & g in L1_Functions M & f a.e.= g,M implies ( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) ) )
assume that
A1: f in L1_Functions M and
A2: g in L1_Functions M and
A3: f a.e.= g,M ; ::_thesis: ( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) )
A4: ex f1 being PartFunc of X,REAL st
( f = f1 & ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) ) by A1;
then consider NDf being Element of S such that
A5: M . NDf = 0 and
A6: dom f = NDf ` and
 f is_integrable_on M ;
A7: abs f is_integrable_on M by A4, Th44;
consider EQ being Element of S such that
A8: M . EQ = 0 and
A9: f | (EQ `) = g | (EQ `) by A3, Def10;
(abs f) | (EQ `) = abs (g | (EQ `)) by A9, RFUNCT_1:46
.= (abs g) | (EQ `) by RFUNCT_1:46 ;
then A10: abs f a.e.= abs g,M by A8, Def10;
A11: ex g1 being PartFunc of X,REAL st
( g = g1 & ex ND being Element of S st
( M . ND = 0 & dom g1 = ND ` & g1 is_integrable_on M ) ) by A2;
then consider NDg being Element of S such that
A12: M . NDg = 0 and
A13: dom g = NDg ` and
 g is_integrable_on M ;
A14: abs g is_integrable_on M by A11, Th44;
 dom (abs g) = NDg ` by A13, VALUED_1:def_11;
then A15: abs g in L1_Functions M by A12, A14;
 dom (abs f) = NDf ` by A6, VALUED_1:def_11;
then  abs f in L1_Functions M by A5, A7;
hence  ( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) ) by A15, A10, Th43; ::_thesis: verum
end;

theorem Th46: :: LPSPACE1:46
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) holds
( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) holds
( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) holds
( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) holds
( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M )
let f, g be PartFunc of X,REAL; ::_thesis: ( ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) implies ( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M ) )
assume  ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) ; ::_thesis: ( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M )
then consider x being VECTOR of (Pre-L-Space M) such that
A1: f in x and
A2: g in x ;
 x in the carrier of (Pre-L-Space M) ;
then  x in CosetSet M by Def18;
then consider h being PartFunc of X,REAL such that
A3: x = a.e-eq-class (h,M) and
 h in L1_Functions M ;
 ex k being PartFunc of X,REAL st
( f = k & k in L1_Functions M & h in L1_Functions M & h a.e.= k,M ) by A1, A3;
then A4: f a.e.= h,M by Th29;
 ex j being PartFunc of X,REAL st
( g = j & j in L1_Functions M & h in L1_Functions M & h a.e.= j,M ) by A2, A3;
hence  ( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M ) by A1, A3, A4, Th30; ::_thesis: verum
end;

theorem Th47: :: LPSPACE1:47
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x holds
( f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x holds
( f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x holds
( f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x holds
( f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M )
let f be PartFunc of X,REAL; ::_thesis: for x being Point of (Pre-L-Space M) st f in x holds
( f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M )
let x be Point of (Pre-L-Space M); ::_thesis: ( f in x implies ( f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M ) )
 x in the carrier of (Pre-L-Space M) ;
then  x in CosetSet M by Def18;
then consider h being PartFunc of X,REAL such that
A1: x = a.e-eq-class (h,M) and
 h in L1_Functions M ;
assume  f in x ; ::_thesis: ( f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M )
then  ex g being PartFunc of X,REAL st
( f = g & g in L1_Functions M & h in L1_Functions M & h a.e.= g,M ) by A1;
then  ex f0 being PartFunc of X,REAL st
( f = f0 & ex ND being Element of S st
( M . ND = 0 & dom f0 = ND ` & f0 is_integrable_on M ) ) ;
hence  ( f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M ) by Th44; ::_thesis: verum
end;

theorem Th48: :: LPSPACE1:48
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x & g in x holds
( f a.e.= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x & g in x holds
( f a.e.= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x & g in x holds
( f a.e.= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x & g in x holds
( f a.e.= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )
let f, g be PartFunc of X,REAL; ::_thesis: for x being Point of (Pre-L-Space M) st f in x & g in x holds
( f a.e.= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )
let x be Point of (Pre-L-Space M); ::_thesis: ( f in x & g in x implies ( f a.e.= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) ) )
assume that
A1: f in x and
A2: g in x ; ::_thesis: ( f a.e.= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )
A3: g in L1_Functions M by A2, Th46;
 ( f a.e.= g,M & f in L1_Functions M ) by A1, A2, Th46;
hence  ( f a.e.= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) ) by A3, Th43, Th45; ::_thesis: verum
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func L-1-Norm M ->  Function of the carrier of (Pre-L-Space M),REAL means :Def19: :: LPSPACE1:def 19
 for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & it . x = Integral (M,(abs f)) );
existence
 ex b1 being Function of the carrier of (Pre-L-Space M),REAL st
for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b1 . x = Integral (M,(abs f)) )
proof
defpred S1[ set , set ] means  ex f being PartFunc of X,REAL st
( f in $1 & $2 = Integral (M,(abs f)) );
A1: for x being Point of (Pre-L-Space M) ex y being Element of REAL st S1[x,y]
proof
let x be Point of (Pre-L-Space M); ::_thesis: ex y being Element of REAL st S1[x,y]
 x in the carrier of (Pre-L-Space M) ;
then  x in CosetSet M by Def18;
then consider f being PartFunc of X,REAL such that
A2: x = a.e-eq-class (f,M) and
A3: f in L1_Functions M ;
 ex f0 being PartFunc of X,REAL st
( f = f0 & ex ND being Element of S st
( M . ND = 0 & dom f0 = ND ` & f0 is_integrable_on M ) ) by A3;
then  Integral (M,(abs f)) in REAL by Th44;
hence  ex y being Element of REAL st S1[x,y] by A2, A3, Th38; ::_thesis: verum
end;
consider f being Function of (Pre-L-Space M),REAL such that
A4: for x being Point of (Pre-L-Space M) holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take  f ; ::_thesis: for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & f . x = Integral (M,(abs f)) )
thus  for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & f . x = Integral (M,(abs f)) ) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the carrier of (Pre-L-Space M),REAL st ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b1 . x = Integral (M,(abs f)) ) ) & ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b2 . x = Integral (M,(abs f)) ) ) holds
b1 = b2
proof
let N1, N2 be Function of the carrier of (Pre-L-Space M),REAL; ::_thesis: ( ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & N1 . x = Integral (M,(abs f)) ) ) & ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & N2 . x = Integral (M,(abs f)) ) ) implies N1 = N2 )
assume A5: ( ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & N1 . x = Integral (M,(abs f)) ) ) & ( for x being Point of (Pre-L-Space M) ex g being PartFunc of X,REAL st
( g in x & N2 . x = Integral (M,(abs g)) ) ) ) ; ::_thesis: N1 = N2
now__::_thesis:_for_x_being_Point_of_(Pre-L-Space_M)_holds_N1_._x_=_N2_._x
let x be Point of (Pre-L-Space M); ::_thesis: N1 . x = N2 . x
 ( ex f being PartFunc of X,REAL st
( f in x & N1 . x = Integral (M,(abs f)) ) & ex g being PartFunc of X,REAL st
( g in x & N2 . x = Integral (M,(abs g)) ) ) by A5;
hence  N1 . x = N2 . x by Th48; ::_thesis: verum
end;
hence  N1 = N2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def19 defines L-1-Norm LPSPACE1:def_19_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Function of the carrier of (Pre-L-Space M),REAL holds
( b4 = L-1-Norm M iff for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b4 . x = Integral (M,(abs f)) ) );

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

:: deftheorem  defines L-1-Space LPSPACE1:def_20_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L-1-Space M = NORMSTR(# the carrier of (Pre-L-Space M), the ZeroF of (Pre-L-Space M), the addF of (Pre-L-Space M), the Mult of (Pre-L-Space M),(L-1-Norm M) #);


theorem Th49: :: LPSPACE1:49
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for x being Point of (L-1-Space M) holds
( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for x being Point of (L-1-Space M) holds
( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for x being Point of (L-1-Space M) holds
( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
let M be sigma_Measure of S; ::_thesis: for x being Point of (L-1-Space M) holds
( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
let x be Point of (L-1-Space M); ::_thesis: ( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
reconsider y = x as Point of (Pre-L-Space M) ;
consider f being PartFunc of X,REAL such that
A1: f in y and
A2: (L-1-Norm M) . y = Integral (M,(abs f)) by Def19;
 y in the carrier of (Pre-L-Space M) ;
then  y in CosetSet M by Def18;
then consider g being PartFunc of X,REAL such that
A3: ( y = a.e-eq-class (g,M) & g in L1_Functions M ) ;
 g in y by A3, Th38;
then  f a.e.= g,M by A1, Th46;
then  x = a.e-eq-class (f,M) by A1, A3, Th39;
hence  ( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) ) by A1, A2, Th48; ::_thesis: verum
end;

theorem Th50: :: LPSPACE1:50
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let f be PartFunc of X,REAL; ::_thesis: for x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let x be Point of (L-1-Space M); ::_thesis: ( f in x implies ( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) )
assume A1: f in x ; ::_thesis: ( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
reconsider y = x as Point of (Pre-L-Space M) ;
 y in the carrier of (Pre-L-Space M) ;
then  y in CosetSet M by Def18;
then consider g being PartFunc of X,REAL such that
A2: ( y = a.e-eq-class (g,M) & g in L1_Functions M ) ;
 g in y by A2, Th38;
then  f a.e.= g,M by A1, Th46;
hence  ( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) by A1, A2, Th39, Th49; ::_thesis: verum
end;

theorem Th51: :: LPSPACE1:51
for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x, y being Point of (L-1-Space M) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
proof
let a be Real; ::_thesis: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x, y being Point of (L-1-Space M) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x, y being Point of (L-1-Space M) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x, y being Point of (L-1-Space M) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL
for x, y being Point of (L-1-Space M) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let f, g be PartFunc of X,REAL; ::_thesis: for x, y being Point of (L-1-Space M) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let x, y be Point of (L-1-Space M); ::_thesis: ( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
set C = CosetSet M;
hereby  ::_thesis: ( f in x implies a (#) f in a * x )
reconsider x1 = x, y1 = y as Point of (Pre-L-Space M) ;
assume that
A1: f in x and
A2: g in y ; ::_thesis: f + g in x + y
 y1 in the carrier of (Pre-L-Space M) ;
then A3: y1 in CosetSet M by Def18;
then consider b being PartFunc of X,REAL such that
A4: y1 = a.e-eq-class (b,M) and
A5: b in L1_Functions M ;
A6: b in y1 by A4, A5, Th38;
 ex r being PartFunc of X,REAL st
( g = r & r in L1_Functions M & b in L1_Functions M & b a.e.= r,M ) by A2, A4;
then A7: a.e-eq-class (b,M) = a.e-eq-class (g,M) by Th39;
 x1 in the carrier of (Pre-L-Space M) ;
then A8: x1 in CosetSet M by Def18;
then consider a being PartFunc of X,REAL such that
A9: x1 = a.e-eq-class (a,M) and
A10: a in L1_Functions M ;
 a in x1 by A9, A10, Th38;
then  (addCoset M) . (x1,y1) = a.e-eq-class ((a + b),M) by A8, A3, A6, Def15;
then A11: x1 + y1 = a.e-eq-class ((a + b),M) by Def18;
 ex r being PartFunc of X,REAL st
( f = r & r in L1_Functions M & a in L1_Functions M & a a.e.= r,M ) by A1, A9;
then  a.e-eq-class (a,M) = a.e-eq-class (f,M) by Th39;
then  a.e-eq-class ((a + b),M) = a.e-eq-class ((f + g),M) by A1, A2, A9, A10, A4, A5, A7, Th41;
hence  f + g in x + y by A1, A2, A9, A4, A11, Th23, Th38; ::_thesis: verum
end;
hereby  ::_thesis: verum
reconsider x1 = x as Point of (Pre-L-Space M) ;
 x1 in the carrier of (Pre-L-Space M) ;
then A12: x1 in CosetSet M by Def18;
then consider f1 being PartFunc of X,REAL such that
A13: x1 = a.e-eq-class (f1,M) and
A14: f1 in L1_Functions M ;
 f1 in x1 by A13, A14, Th38;
then  (lmultCoset M) . (a,x1) = a.e-eq-class ((a (#) f1),M) by A12, Def17;
then A15: a * x1 = a.e-eq-class ((a (#) f1),M) by Def18;
assume A16: f in x ; ::_thesis: a (#) f in a * x
then  ex r being PartFunc of X,REAL st
( f = r & r in L1_Functions M & f1 in L1_Functions M & f1 a.e.= r,M ) by A13;
then  a.e-eq-class (f1,M) = a.e-eq-class (f,M) by Th39;
then  a.e-eq-class ((a (#) f1),M) = a.e-eq-class ((a (#) f),M) by A16, A13, A14, Th42;
hence  a (#) f in a * x by A16, A13, A15, Th24, Th38; ::_thesis: verum
end;
end;

theorem Th52: :: LPSPACE1:52
for r being Real
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st E = dom f & ( for x being set st x in dom f holds
f . x = r ) holds
f is_measurable_on E
proof
let r be Real; ::_thesis: for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st E = dom f & ( for x being set st x in dom f holds
f . x = r ) holds
f is_measurable_on E
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st E = dom f & ( for x being set st x in dom f holds
f . x = r ) holds
f is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for f being PartFunc of X,REAL st E = dom f & ( for x being set st x in dom f holds
f . x = r ) holds
f is_measurable_on E
let E be Element of S; ::_thesis: for f being PartFunc of X,REAL st E = dom f & ( for x being set st x in dom f holds
f . x = r ) holds
f is_measurable_on E
let f be PartFunc of X,REAL; ::_thesis: ( E = dom f & ( for x being set st x in dom f holds
f . x = r ) implies f is_measurable_on E )
assume A1: E = dom f ; ::_thesis: ( ex x being set st
( x in dom f & not f . x = r ) or f is_measurable_on E )
 r in REAL ;
then reconsider r0 = r as R_eal by NUMBERS:31;
set g = R_EAL f;
consider g0 being PartFunc of X,ExtREAL such that
A2: g0 is_simple_func_in S and
A3: dom g0 = E and
A4: for x being set st x in E holds
g0 . x = r0 by MESFUNC5:41;
assume A5: for x being set st x in dom f holds
f . x = r ; ::_thesis: f is_measurable_on E
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(R_EAL_f)_holds_
(R_EAL_f)_._x_=_g0_._x
let x be Element of X; ::_thesis: ( x in dom (R_EAL f) implies (R_EAL f) . x = g0 . x )
assume A6: x in dom (R_EAL f) ; ::_thesis: (R_EAL f) . x = g0 . x
then  (R_EAL f) . x = r by A5;
hence  (R_EAL f) . x = g0 . x by A1, A4, A6; ::_thesis: verum
end;
then  g0 = R_EAL f by A1, A3, PARTFUN1:5;
then  R_EAL f is_measurable_on E by A2, MESFUNC2:34;
hence  f is_measurable_on E by MESFUNC6:def_1; ::_thesis: verum
end;

theorem Th53: :: LPSPACE1:53
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M & Integral (M,(abs f)) = 0 holds
f a.e.= X --> 0,M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M & Integral (M,(abs f)) = 0 holds
f a.e.= X --> 0,M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M & Integral (M,(abs f)) = 0 holds
f a.e.= X --> 0,M
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st f in L1_Functions M & Integral (M,(abs f)) = 0 holds
f a.e.= X --> 0,M
let f be PartFunc of X,REAL; ::_thesis: ( f in L1_Functions M & Integral (M,(abs f)) = 0 implies f a.e.= X --> 0,M )
assume that
A1: f in L1_Functions M and
A2: Integral (M,(abs f)) = 0 ; ::_thesis: f a.e.= X --> 0,M
set g = X --> 0;
defpred S1[ Element of NAT , set ] means ( $2 = great_eq_dom ((abs f),(1 / ($1 + 1))) & M . $2 = 0 );
consider f1 being PartFunc of X,REAL such that
A3: f = f1 and
A4: ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) by A1;
A5: abs f is_integrable_on M by A3, A4, Th44;
then  R_EAL (abs f) is_integrable_on M by MESFUNC6:def_4;
then consider E being Element of S such that
A6: E = dom (R_EAL (abs f)) and
A7: R_EAL (abs f) is_measurable_on E by MESFUNC5:def_17;
A8: abs f is_measurable_on E by A7, MESFUNC6:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(abs_f)_holds_
0_<=_(abs_f)_._x
let x be set ; ::_thesis: ( x in dom (abs f) implies 0 <= (abs f) . x )
assume  x in dom (abs f) ; ::_thesis: 0 <= (abs f) . x
then  (abs f) . x = abs (f . x) by VALUED_1:def_11;
hence  0 <= (abs f) . x by COMPLEX1:46; ::_thesis: verum
end;
then A9: abs f is nonnegative by MESFUNC6:52;
A10: now__::_thesis:_for_n_being_Element_of_NAT_ex_B_being_Element_of_S_st_S1[n,B]
let n be Element of NAT ; ::_thesis: ex B being Element of S st S1[n,B]
set r = 1 / (n + 1);
reconsider Br = E /\ (great_eq_dom ((abs f),(1 / (n + 1)))) as Element of S by A6, A8, MESFUNC6:13;
set g = Br --> (1 / (n + 1));
A11: dom (Br --> (1 / (n + 1))) = Br by FUNCT_2:def_1;
A12: for x being set st x in dom (Br --> (1 / (n + 1))) holds
(Br --> (1 / (n + 1))) . x = 1 / (n + 1) by FUNCOP_1:7;
reconsider g = Br --> (1 / (n + 1)) as PartFunc of X,REAL by RELSET_1:7;
A13: (abs f) | Br is_integrable_on M by A5, MESFUNC6:91;
 for x being set st x in dom g holds
0 <= g . x by A12;
then  g is nonnegative by MESFUNC6:52;
then A14: 0 <= Integral (M,g) by A11, A12, Th52, MESFUNC6:84;
A15: dom (abs g) = dom g by VALUED_1:def_11;
A16: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(abs_g)_holds_
(abs_g)_._x_=_g_._x
let x be Element of X; ::_thesis: ( x in dom (abs g) implies (abs g) . x = g . x )
assume A17: x in dom (abs g) ; ::_thesis: (abs g) . x = g . x
then  (abs g) . x = abs (g . x) by VALUED_1:def_11;
then  (abs g) . x = abs (1 / (n + 1)) by A12, A15, A17;
then  (abs g) . x = 1 / (n + 1) by ABSVALUE:def_1;
hence  (abs g) . x = g . x by A12, A15, A17; ::_thesis: verum
end;
A18: dom ((abs f) | Br) = (dom (abs f)) /\ Br by RELAT_1:61
.= Br by A6, XBOOLE_1:17, XBOOLE_1:28 ;
then A19: dom g = dom ((abs f) | Br) by FUNCT_2:def_1;
A20: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
abs_(g_._x)_<=_((abs_f)_|_Br)_._x
let x be Element of X; ::_thesis: ( x in dom g implies abs (g . x) <= ((abs f) | Br) . x )
assume A21: x in dom g ; ::_thesis: abs (g . x) <= ((abs f) | Br) . x
then  x in E /\ (great_eq_dom ((abs f),(1 / (n + 1)))) by FUNCT_2:def_1;
then  x in great_eq_dom ((abs f),(1 / (n + 1))) by XBOOLE_0:def_4;
then A22: ex y being Real st
( y = (abs f) . x & 1 / (n + 1) <= y ) by MESFUNC6:6;
 abs (g . x) = abs (1 / (n + 1)) by A12, A21;
then  abs (g . x) = 1 / (n + 1) by ABSVALUE:def_1;
hence  abs (g . x) <= ((abs f) | Br) . x by A19, A21, A22, FUNCT_1:47; ::_thesis: verum
end;
 g is_measurable_on Br by A11, A12, Th52;
then  Integral (M,(abs g)) <= Integral (M,((abs f) | Br)) by A11, A18, A13, A20, MESFUNC6:96;
then A23: Integral (M,g) <= Integral (M,((abs f) | Br)) by A15, A16, PARTFUN1:5;
A24: for x being set st x in dom g holds
g . x = 1 / (n + 1) by A11, FUNCOP_1:7;
 Integral (M,((abs f) | Br)) <= Integral (M,((abs f) | E)) by A6, A8, A9, MESFUNC6:87, XBOOLE_1:17;
then  Integral (M,g) = 0 by A2, A6, A23, A14, RELAT_1:68;
then  (R_EAL (1 / (n + 1))) * (M . Br) = 0 by A11, A24, MESFUNC6:97;
then A25: M . Br = 0 ;
 for x being set st x in great_eq_dom ((abs f),(1 / (n + 1))) holds
x in dom (abs f) by MESFUNC6:6;
then  great_eq_dom ((abs f),(1 / (n + 1))) c= E by A6, TARSKI:def_3;
hence  ex B being Element of S st S1[n,B] by A25, XBOOLE_1:28; ::_thesis: verum
end;
consider F being Function of NAT,S such that
A26: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A10);
now__::_thesis:_for_y_being_set_st_y_in_union_(rng_F)_holds_
y_in__{__x_where_x_is_Element_of_X_:_(_x_in_dom_f_&_f_._x_<>_0_)__}_
let y be set ; ::_thesis: ( y in union (rng F) implies y in  {  x where x is Element of X : ( x in dom f & f . x <> 0 )  }  )
assume  y in union (rng F) ; ::_thesis: y in  {  x where x is Element of X : ( x in dom f & f . x <> 0 )  }
then consider B being set  such that
A27: y in B and
A28: B in rng F by TARSKI:def_4;
consider n being set  such that
A29: n in NAT and
A30: B = F . n by A28, FUNCT_2:11;
reconsider m = n as Element of NAT by A29;
A31: y in great_eq_dom ((abs f),(1 / (m + 1))) by A26, A27, A30;
then A32: y in dom (abs f) by MESFUNC6:6;
then A33: y in dom f by VALUED_1:def_11;
A34: (abs f) . y = abs (f . y) by A32, VALUED_1:def_11;
 (abs f) . y <> 0 by A31, MESFUNC1:def_14;
then  f . y <> 0 by A34, ABSVALUE:2;
hence  y in  {  x where x is Element of X : ( x in dom f & f . x <> 0 )  }  by A33; ::_thesis: verum
end;
then A35: union (rng F) c=  {  x where x is Element of X : ( x in dom f & f . x <> 0 )  }  by TARSKI:def_3;
consider ND being Element of S such that
A36: M . ND = 0 and
A37: dom f1 = ND ` and
 f1 is_integrable_on M by A4;
reconsider EQ = (union (rng F)) \/ ND as Element of S ;
A38: EQ ` = (ND `) /\ ((union (rng F)) `) by XBOOLE_1:53;
then A39: EQ ` c= dom f by A3, A37, XBOOLE_1:17;
 dom (X --> 0) = X by FUNCOP_1:13;
then A40: dom ((X --> 0) | (EQ `)) = EQ ` by RELAT_1:62;
A41: dom (f | (EQ `)) = EQ ` by A3, A37, A38, RELAT_1:62, XBOOLE_1:17;
now__::_thesis:_for_y_being_set_st_y_in__{__x_where_x_is_Element_of_X_:_(_x_in_dom_f_&_f_._x_<>_0_)__}__holds_
y_in_union_(rng_F)
let y be set ; ::_thesis: ( y in  {  x where x is Element of X : ( x in dom f & f . x <> 0 )  }  implies y in union (rng F) )
assume  y in  {  x where x is Element of X : ( x in dom f & f . x <> 0 )  }  ; ::_thesis: y in union (rng F)
then consider z being Element of X such that
A42: y = z and
A43: z in dom f and
A44: f . z <> 0 ;
A45: z in dom (abs f) by A43, VALUED_1:def_11;
then  (abs f) . z = abs (f . z) by VALUED_1:def_11;
then  0 < (abs f) . z by A44, COMPLEX1:47;
then consider n being Element of NAT  such that
A46: 1 / (n + 1) < ((abs f) . z) - 0 by MESFUNC1:10;
 z in great_eq_dom ((abs f),(1 / (n + 1))) by A45, A46, MESFUNC6:6;
then A47: y in F . n by A26, A42;
 F . n in rng F by FUNCT_2:4;
hence  y in union (rng F) by A47, TARSKI:def_4; ::_thesis: verum
end;
then   {  x where x is Element of X : ( x in dom f & f . x <> 0 )  }  c= union (rng F) by TARSKI:def_3;
then A48:  {  x where x is Element of X : ( x in dom f & f . x <> 0 )  }  = union (rng F) by A35, XBOOLE_0:def_10;
A49: now__::_thesis:_for_x_being_set_st_x_in_EQ_`_holds_
f_._x_=_0
let x be set ; ::_thesis: ( x in EQ ` implies f . x = 0 )
assume A50: x in EQ ` ; ::_thesis: f . x = 0
then  x in (union (rng F)) ` by A38, XBOOLE_0:def_4;
then  not x in union (rng F) by XBOOLE_0:def_5;
hence  f . x = 0 by A48, A39, A50; ::_thesis: verum
end;
now__::_thesis:_for_y_being_set_st_y_in_dom_(f_|_(EQ_`))_holds_
(f_|_(EQ_`))_._y_=_((X_-->_0)_|_(EQ_`))_._y
let y be set ; ::_thesis: ( y in dom (f | (EQ `)) implies (f | (EQ `)) . y = ((X --> 0) | (EQ `)) . y )
assume A51: y in dom (f | (EQ `)) ; ::_thesis: (f | (EQ `)) . y = ((X --> 0) | (EQ `)) . y
then  (f | (EQ `)) . y = f . y by FUNCT_1:47;
then  (f | (EQ `)) . y = 0 by A41, A49, A51;
then  (f | (EQ `)) . y = (X --> 0) . y by A51, FUNCOP_1:7;
hence  (f | (EQ `)) . y = ((X --> 0) | (EQ `)) . y by A41, A40, A51, FUNCT_1:47; ::_thesis: verum
end;
then A52: f | (EQ `) = (X --> 0) | (EQ `) by A39, A40, FUNCT_1:2, RELAT_1:62;
now__::_thesis:_for_A_being_set_st_A_in_rng_F_holds_
A_is_measure_zero_of_M
let A be set ; ::_thesis: ( A in rng F implies A is measure_zero of M )
assume  A in rng F ; ::_thesis: A is measure_zero of M
then consider n being set  such that
A53: n in NAT and
A54: A = F . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A53;
 M . (F . n) = 0 by A26;
hence  A is measure_zero of M by A54, MEASURE1:def_7; ::_thesis: verum
end;
then A55: union (rng F) is measure_zero of M by MEASURE2:14;
 ND is measure_zero of M by A36, MEASURE1:def_7;
then  EQ is measure_zero of M by A55, MEASURE1:37;
then  M . EQ = 0 by MEASURE1:def_7;
hence  f a.e.= X --> 0,M by A52, Def10; ::_thesis: verum
end;

theorem Th54: :: LPSPACE1:54
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds Integral (M,(abs (X --> 0))) = 0
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S holds Integral (M,(abs (X --> 0))) = 0
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S holds Integral (M,(abs (X --> 0))) = 0
let M be sigma_Measure of S; ::_thesis: Integral (M,(abs (X --> 0))) = 0
set f = X --> 0;
A1: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(abs_(X_-->_0))_holds_
(abs_(X_-->_0))_._x_=_0
let x be Element of X; ::_thesis: ( x in dom (abs (X --> 0)) implies (abs (X --> 0)) . x = 0 )
 (X --> 0) . x = 0 by FUNCOP_1:7;
then A2: abs ((X --> 0) . x) = 0 by ABSVALUE:2;
assume  x in dom (abs (X --> 0)) ; ::_thesis: (abs (X --> 0)) . x = 0
hence  (abs (X --> 0)) . x = 0 by A2, VALUED_1:def_11; ::_thesis: verum
end;
 dom (X --> 0) = X by FUNCOP_1:13;
then  dom (abs (X --> 0)) = X by VALUED_1:def_11;
hence  Integral (M,(abs (X --> 0))) = 0 by A1, Lm2; ::_thesis: verum
end;

theorem Th55: :: LPSPACE1:55
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g))) )
set f1 = R_EAL f;
set g1 = R_EAL g;
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
A3: R_EAL f is_integrable_on M by A1, MESFUNC6:def_4;
then consider B being Element of S such that
A4: B = dom (R_EAL f) and
A5: R_EAL f is_measurable_on B by MESFUNC5:def_17;
A6: B = dom |.(R_EAL f).| by A4, MESFUNC1:def_10;
 |.(R_EAL f).| is_integrable_on M by A3, A4, A5, MESFUNC5:100;
then A7: ex E being Element of S st
( E = dom |.(R_EAL f).| & |.(R_EAL f).| is_measurable_on E ) by MESFUNC5:def_17;
A8: R_EAL g is_integrable_on M by A2, MESFUNC6:def_4;
then consider C being Element of S such that
A9: C = dom (R_EAL g) and
A10: R_EAL g is_measurable_on C by MESFUNC5:def_17;
A11: C = dom |.(R_EAL g).| by A9, MESFUNC1:def_10;
consider E being Element of S such that
A12: E = dom ((R_EAL f) + (R_EAL g)) and
A13: Integral (M,(|.((R_EAL f) + (R_EAL g)).| | E)) <= (Integral (M,(|.(R_EAL f).| | E))) + (Integral (M,(|.(R_EAL g).| | E))) by A3, A8, MESFUNC7:22;
 dom |.((R_EAL f) + (R_EAL g)).| = E by A12, MESFUNC1:def_10;
then  ( (R_EAL f) + (R_EAL g) = R_EAL (f + g) & |.((R_EAL f) + (R_EAL g)).| | E = |.((R_EAL f) + (R_EAL g)).| ) by MESFUNC6:23, RELAT_1:68;
then A14: Integral (M,(|.((R_EAL f) + (R_EAL g)).| | E)) = Integral (M,|.(f + g).|) by MESFUNC6:1;
 |.(R_EAL g).| is_integrable_on M by A8, A9, A10, MESFUNC5:100;
then A15: ex E being Element of S st
( E = dom |.(R_EAL g).| & |.(R_EAL g).| is_measurable_on E ) by MESFUNC5:def_17;
A16: E = ((dom (R_EAL f)) /\ (dom (R_EAL g))) \ ((((R_EAL f) " {-infty}) /\ ((R_EAL g) " {+infty})) \/ (((R_EAL f) " {+infty}) /\ ((R_EAL g) " {-infty}))) by A12, MESFUNC1:def_3;
then  E c= dom (R_EAL g) by XBOOLE_1:18, XBOOLE_1:36;
then  E c= dom |.(R_EAL g).| by MESFUNC1:def_10;
then  Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,(|.(R_EAL g).| | C)) by A11, A15, MESFUNC5:93;
then  Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,|.(R_EAL g).|) by A11, RELAT_1:68;
then A17: Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,|.g.|) by MESFUNC6:1;
 E c= dom (R_EAL f) by A16, XBOOLE_1:18, XBOOLE_1:36;
then  E c= dom |.(R_EAL f).| by MESFUNC1:def_10;
then  Integral (M,(|.(R_EAL f).| | E)) <= Integral (M,(|.(R_EAL f).| | B)) by A6, A7, MESFUNC5:93;
then  Integral (M,(|.(R_EAL f).| | E)) <= Integral (M,|.(R_EAL f).|) by A6, RELAT_1:68;
then  Integral (M,(|.(R_EAL f).| | E)) <= Integral (M,|.f.|) by MESFUNC6:1;
then  (Integral (M,(|.(R_EAL f).| | E))) + (Integral (M,(|.(R_EAL g).| | E))) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|)) by A17, XXREAL_3:36;
hence  Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g))) by A13, A14, XXREAL_0:2; ::_thesis: verum
end;

Lm7:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )
let M be sigma_Measure of S; ::_thesis: ( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )
now__::_thesis:_for_x,_y_being_Point_of_(L-1-Space_M)
for_a_being_Real_holds_
(_(_||.x.||_=_0_implies_x_=_0._(L-1-Space_M)_)_&_(_x_=_0._(L-1-Space_M)_implies_||.x.||_=_0_)_&_0_<=_||.x.||_&_||.(x_+_y).||_<=_||.x.||_+_||.y.||_&_||.(a_*_x).||_=_(abs_a)_*_||.x.||_)
let x, y be Point of (L-1-Space M); ::_thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (L-1-Space M) ) & ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
let a be Real; ::_thesis: ( ( ||.x.|| = 0 implies x = 0. (L-1-Space M) ) & ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
consider f being PartFunc of X,REAL such that
A1: f in x and
A2: ||.x.|| = Integral (M,(abs f)) by Def19;
 abs f is_integrable_on M by A1, Th47;
then  Integral (M,((abs a) (#) (abs f))) = (R_EAL (abs a)) * (Integral (M,(abs f))) by MESFUNC6:102;
then  Integral (M,(abs (a (#) f))) = (R_EAL (abs a)) * (Integral (M,(abs f))) by RFUNCT_1:25;
then A3: Integral (M,(abs (a (#) f))) = (abs a) * ||.x.|| by A2, EXTREAL1:1;
hereby  ::_thesis: ( ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
set g = X --> 0;
reconsider x1 = x as Point of (Pre-L-Space M) ;
consider f being PartFunc of X,REAL such that
A4: f in x1 and
 (L-1-Norm M) . x1 = Integral (M,(abs f)) by Def19;
A5: f in L1_Functions M by A4, Th47;
then A6: a.e-eq-class (f,M) in CosetSet M ;
A7: X --> 0 in L1_Functions M by Lm3;
assume  ||.x.|| = 0 ; ::_thesis: x = 0. (L-1-Space M)
then  Integral (M,(abs f)) = 0 by A4, Th49;
then  f a.e.= X --> 0,M by A5, Th53;
then  a.e-eq-class ((X --> 0),M) = a.e-eq-class (f,M) by A5, A7, Th39;
then  zeroCoset M = a.e-eq-class (f,M) by A7, A6, Def16;
then  0. (Pre-L-Space M) = a.e-eq-class (f,M) by Def18;
hence  x = 0. (L-1-Space M) by A4, Th50; ::_thesis: verum
end;
hereby  ::_thesis: ( 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
reconsider x1 = x as Point of (Pre-L-Space M) ;
consider f being PartFunc of X,REAL such that
A8: f = X --> 0 and
A9: ( f in L1_Functions M & zeroCoset M = a.e-eq-class (f,M) ) by Def16;
assume  x = 0. (L-1-Space M) ; ::_thesis: ||.x.|| = 0
then  x1 = 0. (Pre-L-Space M) ;
then A10: x1 = zeroCoset M by Def18;
 (L-1-Norm M) . x1 = ||.x.|| ;
then  (L-1-Norm M) . x1 = Integral (M,(abs f)) by A10, A9, Th38, Th49;
hence  ||.x.|| = 0 by A8, Th54; ::_thesis: verum
end;
A11: f is_integrable_on M by A1, Th47;
then  |.(Integral (M,f)).| <= Integral (M,(abs f)) by MESFUNC6:95;
hence  0 <= ||.x.|| by A2, EXTREAL2:3; ::_thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
consider g being PartFunc of X,REAL such that
A12: g in y and
A13: ||.y.|| = Integral (M,(abs g)) by Def19;
A14: g is_integrable_on M by A12, Th47;
 f + g in x + y by A1, A12, Th51;
then A15: ||.(x + y).|| = Integral (M,(abs (f + g))) by Th49;
 (Integral (M,(abs f))) + (Integral (M,(abs g))) = ||.x.|| + ||.y.|| by A2, A13, SUPINF_2:1;
hence  ||.(x + y).|| <= ||.x.|| + ||.y.|| by A11, A15, A14, Th55; ::_thesis: ||.(a * x).|| = (abs a) * ||.x.||
 a (#) f in a * x by A1, Th51;
hence  ||.(a * x).|| = (abs a) * ||.x.|| by A3, Th49; ::_thesis: verum
end;
hence  ( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable ) by NORMSP_1:def_1, RSSPACE3:2; ::_thesis: verum
end;

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster L-1-Space M ->  non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealNormSpace-like ;
coherence
 ( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable ) by Lm7;
end;