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 Th71;

now :: thesis: for A, B being Element of CosetSet M holds (addCoset M) . (A,B) = (addCoset (M,1)) . (A,B)

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 ) ;
A4: ( A is Element of CosetSet (M,1) & B is Element of CosetSet (M,1) ) by Th71;
A5: ( a in a.e-eq-class (a,M) & b in a.e-eq-class (b,M) ) by A2, A3, LPSPACE1:38;
then A6: (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 E -measurable ) by Lm8;
then (addCoset M) . (A,B) = a.e-eq-class_Lp ((a + b),M,1) by A6, Lm12;
hence (addCoset M) . (A,B) = (addCoset (M,1)) . (A,B) by A4, A5, A2, A3, Def8; :: thesis: verum

end;

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