let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
set Z = AlmostZeroFunctions M;
set V = RLSp_L1Funct M;

let v, u be VECTOR of (RLSp_L1Funct M); :: thesis:
assume that
A1: v in AlmostZeroFunctions M and
A2: u in AlmostZeroFunctions M ; :: thesis:
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:

end;

hence AlmostZeroFunctions M is add-closed ; :: thesis:

let a be Real; :: thesis:
let u be VECTOR of (RLSp_L1Funct M); :: thesis:
assume u in AlmostZeroFunctions M ; :: thesis:
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:

end;

hence AlmostZeroFunctions M is multi-closed ; :: thesis: