let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real holds
( Lp_Functions M,k is add-closed & Lp_Functions M,k is multi-closed )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for k being positive Real holds
( Lp_Functions M,k is add-closed & Lp_Functions M,k is multi-closed )
let M be sigma_Measure of S; :: thesis: for k being positive Real holds
( Lp_Functions M,k is add-closed & Lp_Functions M,k is multi-closed )
let k be positive Real; :: thesis: ( Lp_Functions M,k is add-closed & Lp_Functions M,k is multi-closed )
set W = Lp_Functions M,k;

now

let v, u be Element of the carrier of (RLSp_PFunct X); :: thesis: ( v in Lp_Functions M,k & u in Lp_Functions M,k implies v + u in Lp_Functions M,k )
assume A2: ( v in Lp_Functions M,k & u in Lp_Functions M,k ) ; :: thesis: v + u in Lp_Functions M,k
then consider v1 being PartFunc of X,REAL such that
A3: ( v1 = v & ex ND being Element of S st
( M . (ND ` ) = 0 & dom v1 = ND & v1 is_measurable_on ND & (abs v1) to_power k is_integrable_on M ) ) ;
consider u1 being PartFunc of X,REAL such that
A4: ( u1 = u & ex ND being Element of S st
( M . (ND ` ) = 0 & dom u1 = ND & u1 is_measurable_on ND & (abs u1) to_power k is_integrable_on M ) ) by A2;
reconsider h = v + u as Element of PFuncs X,REAL ;
( 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, LPSPACE1:6;
then v + u = v1 + u1 by VALUED_1:def 1;
hence v + u in Lp_Functions M,k by A2, A3, A4, Th01aLp; :: thesis: verum

end;

hence Lp_Functions M,k is add-closed by IDEAL_1:def 1; :: thesis: Lp_Functions M,k is multi-closed

now

let a be Real; :: thesis: for u being VECTOR of (RLSp_PFunct X) st u in Lp_Functions M,k holds
a * u in Lp_Functions M,k
let u be VECTOR of (RLSp_PFunct X); :: thesis: ( u in Lp_Functions M,k implies a * u in Lp_Functions M,k )
assume A7: u in Lp_Functions M,k ; :: thesis: a * u in Lp_Functions M,k
then consider u1 being PartFunc of X,REAL such that
A8: ( u1 = u & ex ND being Element of S st
( M . (ND ` ) = 0 & dom u1 = ND & u1 is_measurable_on ND & (abs u1) to_power k is_integrable_on M ) ) ;
reconsider h = a * u as Element of PFuncs X,REAL ;
A9: ( dom h = dom u1 & ( for x being Element of X st x in dom u1 holds
h . x = a * (u1 . x) ) ) by A8, LPSPACE1:9;
then for x being set st x in dom h holds
h . x = a * (u1 . x) ;
then a * u = a (#) u1 by A9, VALUED_1:def 5;
hence a * u in Lp_Functions M,k by Th01bLp, A7, A8; :: thesis: verum

end;

hence Lp_Functions M,k is multi-closed by LPSPACE1:def 1; :: thesis: verum