let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds
( AlmostZeroCFunctions M is add-closed & AlmostZeroCFunctions M is multi-closed )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds
( AlmostZeroCFunctions M is add-closed & AlmostZeroCFunctions M is multi-closed )
let M be sigma_Measure of S; :: thesis: ( AlmostZeroCFunctions M is add-closed & AlmostZeroCFunctions M is multi-closed )
set Z = AlmostZeroCFunctions M;
set V = CLSp_L1Funct M;

now :: thesis: for v, u being VECTOR of (CLSp_L1Funct M) st v in AlmostZeroCFunctions M & u in AlmostZeroCFunctions M holds
v + u in AlmostZeroCFunctions M

let v, u be VECTOR of (CLSp_L1Funct M); :: thesis: ( v in AlmostZeroCFunctions M & u in AlmostZeroCFunctions M implies v + u in AlmostZeroCFunctions M )
assume that
A1: v in AlmostZeroCFunctions M and
A2: u in AlmostZeroCFunctions M ; :: thesis: v + u in AlmostZeroCFunctions M
consider v1 being PartFunc of X,COMPLEX such that
A3: v1 = v and
v1 in L1_CFunctions M and
A4: v1 a.e.cpfunc= X --> 0c,M by A1;
consider u1 being PartFunc of X,COMPLEX such that
A5: u1 = u and
u1 in L1_CFunctions M and
A6: u1 a.e.cpfunc= X --> 0c,M by A2;
A7: v + u = v1 + u1 by A3, A5, Th19;
(X --> 0c) + (X --> 0c) = X --> 0c by Th27;
then v1 + u1 a.e.cpfunc= X --> 0c,M by A4, A6, Th25;
hence v + u in AlmostZeroCFunctions M by A7; :: thesis: verum

end;

hence AlmostZeroCFunctions M is add-closed ; :: thesis: AlmostZeroCFunctions M is multi-closed

now :: thesis: for a being Complex
for u being VECTOR of (CLSp_L1Funct M) st u in AlmostZeroCFunctions M holds
a * u in AlmostZeroCFunctions M

let a be Complex; :: thesis: for u being VECTOR of (CLSp_L1Funct M) st u in AlmostZeroCFunctions M holds
a * u in AlmostZeroCFunctions M
let u be VECTOR of (CLSp_L1Funct M); :: thesis: ( u in AlmostZeroCFunctions M implies a * u in AlmostZeroCFunctions M )
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;
assume u in AlmostZeroCFunctions M ; :: thesis: a * u in AlmostZeroCFunctions M
then consider u1 being PartFunc of X,COMPLEX such that
A8: u1 = u and
u1 in L1_CFunctions M and
A9: u1 a.e.cpfunc= X --> 0c,M ;
A10: a1 * u = a (#) u1 by A8, Th20;
a1 (#) (X --> 0) = X --> 0 by Th27;
then a1 (#) u1 a.e.cpfunc= X --> 0c,M by A9, Th26;
hence a * u in AlmostZeroCFunctions M by A10; :: thesis: verum

end;

hence AlmostZeroCFunctions M is multi-closed ; :: thesis: verum