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

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 :: thesis: for v, u being Element of the carrier of (RLSp_PFunct X) st v in Lp_Functions (M,k) & u in Lp_Functions (M,k) holds

v + u in Lp_Functions (M,k)

hence
Lp_Functions (M,k) is add-closed
by IDEAL_1:def 1; :: thesis: Lp_Functions (M,k) is multi-closed v + u in Lp_Functions (M,k)

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

A2: ( v1 = v & ex ND being Element of S st

( M . (ND `) = 0 & dom v1 = ND & v1 is ND -measurable & (abs v1) to_power k is_integrable_on M ) ) ;

consider u1 being PartFunc of X,REAL such that

A3: ( u1 = u & ex ND being Element of S st

( M . (ND `) = 0 & dom u1 = ND & u1 is ND -measurable & (abs u1) to_power k is_integrable_on M ) ) by A1;

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

( dom h = (dom v1) /\ (dom u1) & ( for x being object st x in dom h holds

h . x = (v1 . x) + (u1 . x) ) ) by A2, A3, LPSPACE1:6;

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

hence v + u in Lp_Functions (M,k) by A1, A2, A3, Th25; :: thesis: verum

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

A2: ( v1 = v & ex ND being Element of S st

( M . (ND `) = 0 & dom v1 = ND & v1 is ND -measurable & (abs v1) to_power k is_integrable_on M ) ) ;

consider u1 being PartFunc of X,REAL such that

A3: ( u1 = u & ex ND being Element of S st

( M . (ND `) = 0 & dom u1 = ND & u1 is ND -measurable & (abs u1) to_power k is_integrable_on M ) ) by A1;

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

( dom h = (dom v1) /\ (dom u1) & ( for x being object st x in dom h holds

h . x = (v1 . x) + (u1 . x) ) ) by A2, A3, LPSPACE1:6;

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

hence v + u in Lp_Functions (M,k) by A1, A2, A3, Th25; :: thesis: verum

now :: thesis: for a being Real

for u being VECTOR of (RLSp_PFunct X) st u in Lp_Functions (M,k) holds

a * u in Lp_Functions (M,k)

hence
Lp_Functions (M,k) is multi-closed
; :: thesis: verumfor u being VECTOR of (RLSp_PFunct X) st u in Lp_Functions (M,k) holds

a * u in Lp_Functions (M,k)

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 A4: u in Lp_Functions (M,k) ; :: thesis: a * u in Lp_Functions (M,k)

then consider u1 being PartFunc of X,REAL such that

A5: ( u1 = u & ex ND being Element of S st

( M . (ND `) = 0 & dom u1 = ND & u1 is ND -measurable & (abs u1) to_power k is_integrable_on M ) ) ;

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

A6: ( dom h = dom u1 & ( for x being Element of X st x in dom u1 holds

h . x = a * (u1 . x) ) ) by A5, LPSPACE1:9;

then for x being object st x in dom h holds

h . x = a * (u1 . x) ;

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

hence a * u in Lp_Functions (M,k) by Th26, A4, A5; :: thesis: verum

end;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 A4: u in Lp_Functions (M,k) ; :: thesis: a * u in Lp_Functions (M,k)

then consider u1 being PartFunc of X,REAL such that

A5: ( u1 = u & ex ND being Element of S st

( M . (ND `) = 0 & dom u1 = ND & u1 is ND -measurable & (abs u1) to_power k is_integrable_on M ) ) ;

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

A6: ( dom h = dom u1 & ( for x being Element of X st x in dom u1 holds

h . x = a * (u1 . x) ) ) by A5, LPSPACE1:9;

then for x being object st x in dom h holds

h . x = a * (u1 . x) ;

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

hence a * u in Lp_Functions (M,k) by Th26, A4, A5; :: thesis: verum