let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds addCoset M = addCoset M,1
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds addCoset M = addCoset M,1
let M be sigma_Measure of S; :: thesis: addCoset M = addCoset M,1
A1: CosetSet M = CosetSet M,1 by Th9a;

now

let A, B be Element of CosetSet M; :: thesis: (addCoset M) . A,B = (addCoset M,1) . A,B
A in { (a.e-eq-class f,M) where f is PartFunc of X,REAL : f in L1_Functions M } ;
then consider a being PartFunc of X,REAL such that
A2: ( A = a.e-eq-class a,M & a in L1_Functions M ) ;
B in { (a.e-eq-class f,M) where f is PartFunc of X,REAL : f in L1_Functions M } ;
then consider b being PartFunc of X,REAL such that
A3: ( B = a.e-eq-class b,M & b in L1_Functions M ) ;
B1: ( A is Element of CosetSet M,1 & B is Element of CosetSet M,1 ) by Th9a;
B2: ( a in a.e-eq-class a,M & b in a.e-eq-class b,M ) by A2, A3, LPSPACE1:38;
then A4: (addCoset M) . A,B = a.e-eq-class (a + b),M by A2, A3, LPSPACE1:def 15;
a + b in L1_Functions M by A2, A3, LPSPACE1:23;
then ex E being Element of S st
( M . (E ` ) = 0 & E = dom (a + b) & a + b is_measurable_on E ) by Lem00;
then (addCoset M) . A,B = a.e-eq-class_Lp (a + b),M,1 by A4, Lem03;
hence (addCoset M) . A,B = (addCoset M,1) . A,B by B1, B2, A2, A3, VSPDef3X; :: thesis: verum

end;

hence addCoset M = addCoset M,1 by A1, BINOP_1:2; :: thesis: verum