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;

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)

hence
addCoset M = addCoset (M,1)
by A1, BINOP_1:2; :: thesis: verumlet 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;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