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

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 A2: ( v in AlmostZeroFunctions M & u in AlmostZeroFunctions M ) ; :: thesis: v + u in AlmostZeroFunctions M
consider v1 being PartFunc of X,REAL such that
A3: ( v1 = v & v1 in L1_Functions M & v1 a.e.= X --> 0 ,M ) by A2;
consider u1 being PartFunc of X,REAL such that
A4: ( u1 = u & u1 in L1_Functions M & u1 a.e.= X --> 0 ,M ) by A2;
A5: v + u = v1 + u1 by ThB10, A3, A4;
(X --> 0 ) + (X --> 0 ) = X --> 0 by HSATZE;
then ( v1 + u1 in L1_Functions M & v1 + u1 a.e.= X --> 0 ,M ) by A5, A3, A4, Th07;
hence v + u in AlmostZeroFunctions M by A5; :: thesis: verum

end;

hence AlmostZeroFunctions M is add-closed by IDEAL_1:def 1; :: thesis: AlmostZeroFunctions M is multi-closed

now

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
A10: ( u1 = u & u1 in L1_Functions M & u1 a.e.= X --> 0 ,M ) ;
A11: a * u = a (#) u1 by ThB11, A10;
a (#) (X --> 0 ) = X --> 0 by HSATZE;
then ( a (#) u1 in L1_Functions M & a (#) u1 a.e.= X --> 0 ,M ) by A11, A10, Th08;
hence a * u in AlmostZeroFunctions M by A11; :: thesis: verum

end;

hence AlmostZeroFunctions M is multi-closed by RLSUBDef0; :: thesis: verum