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 () . (A,B) = (addCoset (M,1)) . (A,B)
let A, B be Element of CosetSet M; :: thesis: () . (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 ;
then A6: (addCoset M) . (A,B) = a.e-eq-class ((a + b),M) by ;
a + b in L1_Functions M by ;
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 ;
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 ; :: thesis: verum