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 ; :: 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 ; :: thesis: verum