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
( AlmostZeroLpFunctions M,k is add-closed & AlmostZeroLpFunctions 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
( AlmostZeroLpFunctions M,k is add-closed & AlmostZeroLpFunctions M,k is multi-closed )
let M be sigma_Measure of S; :: thesis: for k being positive Real holds
( AlmostZeroLpFunctions M,k is add-closed & AlmostZeroLpFunctions M,k is multi-closed )
let k be positive Real; :: thesis: ( AlmostZeroLpFunctions M,k is add-closed & AlmostZeroLpFunctions M,k is multi-closed )
set Z = AlmostZeroLpFunctions M,k;
set V = RLSp_LpFunct M,k;

now

let v, u be VECTOR of (RLSp_LpFunct M,k); :: thesis: ( v in AlmostZeroLpFunctions M,k & u in AlmostZeroLpFunctions M,k implies v + u in AlmostZeroLpFunctions M,k )
assume A2: ( v in AlmostZeroLpFunctions M,k & u in AlmostZeroLpFunctions M,k ) ; :: thesis: v + u in AlmostZeroLpFunctions M,k
then consider v1 being PartFunc of X,REAL such that
A3: ( v1 = v & v1 in Lp_Functions M,k & v1 a.e.= X --> 0 ,M ) ;
consider u1 being PartFunc of X,REAL such that
A4: ( u1 = u & u1 in Lp_Functions M,k & u1 a.e.= X --> 0 ,M ) by A2;
A5: v + u = v1 + u1 by ThB10, A3, A4;
(X --> 0 ) + (X --> 0 ) = X --> 0 by LPSPACE1:33;
then ( v1 + u1 in Lp_Functions M,k & v1 + u1 a.e.= X --> 0 ,M ) by A5, A3, A4, LPSPACE1:31;
hence v + u in AlmostZeroLpFunctions M,k by A5; :: thesis: verum

end;

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

now

let a be Real; :: thesis: for u being VECTOR of (RLSp_LpFunct M,k) st u in AlmostZeroLpFunctions M,k holds
a * u in AlmostZeroLpFunctions M,k
let u be VECTOR of (RLSp_LpFunct M,k); :: thesis: ( u in AlmostZeroLpFunctions M,k implies a * u in AlmostZeroLpFunctions M,k )
assume u in AlmostZeroLpFunctions M,k ; :: thesis: a * u in AlmostZeroLpFunctions M,k
then consider u1 being PartFunc of X,REAL such that
A10: ( u1 = u & u1 in Lp_Functions M,k & u1 a.e.= X --> 0 ,M ) ;
A11: a * u = a (#) u1 by ThB11, A10;
a (#) (X --> 0 ) = X --> 0 by LPSPACE1:33;
then ( a (#) u1 in Lp_Functions M,k & a (#) u1 a.e.= X --> 0 ,M ) by A11, A10, LPSPACE1:32;
hence a * u in AlmostZeroLpFunctions M,k by A11; :: thesis: verum

end;

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