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

now :: thesis: for v, u being Element of (CLSp_PFunct X) st v in L1_CFunctions M & u in L1_CFunctions M holds
v + u in L1_CFunctions M

let v, u be Element of (CLSp_PFunct X); :: thesis: ( v in L1_CFunctions M & u in L1_CFunctions M implies v + u in L1_CFunctions M )
assume that
A1: v in L1_CFunctions M and
A2: u in L1_CFunctions M ; :: thesis: v + u in L1_CFunctions M
reconsider h = v + u as Element of PFuncs (X,COMPLEX) ;
consider v1 being PartFunc of X,COMPLEX such that
A3: v1 = v and
ex ND being Element of S st
( M . ND = 0 & dom v1 = ND ` & v1 is_integrable_on M ) by A1;
consider u1 being PartFunc of X,COMPLEX such that
A4: u1 = u and
ex ND being Element of S st
( M . ND = 0 & dom u1 = ND ` & u1 is_integrable_on M ) by A2;
( dom h = (dom v1) /\ (dom u1) & ( for x being object st x in dom h holds
h . x = (v1 . x) + (u1 . x) ) ) by A3, A4, Th4;
then v + u = v1 + u1 by VALUED_1:def 1;
hence v + u in L1_CFunctions M by A1, A2, A3, A4, Th17; :: thesis: verum

end;

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

now :: thesis: for a being Complex
for u being VECTOR of (CLSp_PFunct X) st u in L1_CFunctions M holds
a * u in L1_CFunctions M

let a be Complex; :: thesis: for u being VECTOR of (CLSp_PFunct X) st u in L1_CFunctions M holds
a * u in L1_CFunctions M
let u be VECTOR of (CLSp_PFunct X); :: thesis: ( u in L1_CFunctions M implies a * u in L1_CFunctions M )
assume A5: u in L1_CFunctions M ; :: thesis: a * u in L1_CFunctions M
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;
consider u1 being PartFunc of X,COMPLEX such that
A6: u1 = u and
ex ND being Element of S st
( M . ND = 0 & dom u1 = ND ` & u1 is_integrable_on M ) by A5;
reconsider h = a1 * u as Element of PFuncs (X,COMPLEX) ;
A7: a1 * u = (multcomplexcpfunc X) . (a,u) ;
then A8: dom h = dom u1 by A6, Th7;
then for x being object st x in dom h holds
h . x = a * (u1 . x) by A6, A7, Th7;
then a1 * u = a (#) u1 by A8, VALUED_1:def 5;
hence a * u in L1_CFunctions M by A5, A6, Th18; :: thesis: verum

end;

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