let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds

f - g a.e.= (X --> 0) | E,M

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds

f - g a.e.= (X --> 0) | E,M

let M be sigma_Measure of S; :: thesis: for E being Element of S

for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds

f - g a.e.= (X --> 0) | E,M

let E be Element of S; :: thesis: for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds

f - g a.e.= (X --> 0) | E,M

let f, g be PartFunc of X,REAL; :: thesis: ( ( E = dom f or E = dom g ) & f a.e.= g,M implies f - g a.e.= (X --> 0) | E,M )

assume that

A1: ( E = dom f or E = dom g ) and

A2: f a.e.= g,M ; :: thesis: f - g a.e.= (X --> 0) | E,M

consider A being Element of S such that

A3: ( M . A = 0 & f | (A `) = g | (A `) ) by A2, LPSPACE1:def 10;

A4: (dom f) /\ (A `) = dom (g | (A `)) by A3, RELAT_1:61

.= (dom g) /\ (A `) by RELAT_1:61 ;

A5: dom ((f - g) | (A `)) = (dom (f - g)) /\ (A `) by RELAT_1:61;

then A6: dom ((f - g) | (A `)) = ((dom f) /\ (dom g)) /\ (A `) by VALUED_1:12

.= ((dom f) /\ (A `)) /\ ((dom f) /\ (A `)) by A4, XBOOLE_1:116 ;

A7: dom ((f - g) | (A `)) = ((dom f) /\ (dom g)) /\ (A `) by A5, VALUED_1:12

.= ((dom g) /\ (A `)) /\ ((dom g) /\ (A `)) by A4, XBOOLE_1:116 ;

A8: dom (((X --> 0) | E) | (A `)) = (dom ((X --> 0) | E)) /\ (A `) by RELAT_1:61

.= ((dom (X --> 0)) /\ E) /\ (A `) by RELAT_1:61

.= E /\ (A `) by XBOOLE_1:28 ;

for x being Element of X st x in dom ((f - g) | (A `)) holds

((f - g) | (A `)) . x = (((X --> 0) | E) | (A `)) . x

for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds

f - g a.e.= (X --> 0) | E,M

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds

f - g a.e.= (X --> 0) | E,M

let M be sigma_Measure of S; :: thesis: for E being Element of S

for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds

f - g a.e.= (X --> 0) | E,M

let E be Element of S; :: thesis: for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds

f - g a.e.= (X --> 0) | E,M

let f, g be PartFunc of X,REAL; :: thesis: ( ( E = dom f or E = dom g ) & f a.e.= g,M implies f - g a.e.= (X --> 0) | E,M )

assume that

A1: ( E = dom f or E = dom g ) and

A2: f a.e.= g,M ; :: thesis: f - g a.e.= (X --> 0) | E,M

consider A being Element of S such that

A3: ( M . A = 0 & f | (A `) = g | (A `) ) by A2, LPSPACE1:def 10;

A4: (dom f) /\ (A `) = dom (g | (A `)) by A3, RELAT_1:61

.= (dom g) /\ (A `) by RELAT_1:61 ;

A5: dom ((f - g) | (A `)) = (dom (f - g)) /\ (A `) by RELAT_1:61;

then A6: dom ((f - g) | (A `)) = ((dom f) /\ (dom g)) /\ (A `) by VALUED_1:12

.= ((dom f) /\ (A `)) /\ ((dom f) /\ (A `)) by A4, XBOOLE_1:116 ;

A7: dom ((f - g) | (A `)) = ((dom f) /\ (dom g)) /\ (A `) by A5, VALUED_1:12

.= ((dom g) /\ (A `)) /\ ((dom g) /\ (A `)) by A4, XBOOLE_1:116 ;

A8: dom (((X --> 0) | E) | (A `)) = (dom ((X --> 0) | E)) /\ (A `) by RELAT_1:61

.= ((dom (X --> 0)) /\ E) /\ (A `) by RELAT_1:61

.= E /\ (A `) by XBOOLE_1:28 ;

for x being Element of X st x in dom ((f - g) | (A `)) holds

((f - g) | (A `)) . x = (((X --> 0) | E) | (A `)) . x

proof

hence
f - g a.e.= (X --> 0) | E,M
by A3, A7, A1, A6, A8, PARTFUN1:5, LPSPACE1:def 10; :: thesis: verum
let x be Element of X; :: thesis: ( x in dom ((f - g) | (A `)) implies ((f - g) | (A `)) . x = (((X --> 0) | E) | (A `)) . x )

assume A9: x in dom ((f - g) | (A `)) ; :: thesis: ((f - g) | (A `)) . x = (((X --> 0) | E) | (A `)) . x

then A10: x in E by A7, A1, A6, XBOOLE_0:def 4;

A11: ( x in dom (f - g) & x in A ` ) by A5, A9, XBOOLE_0:def 4;

then A12: ((f - g) | (A `)) . x = (f - g) . x by FUNCT_1:49

.= (f . x) - (g . x) by A11, VALUED_1:13

.= ((f | (A `)) . x) - (g . x) by A11, FUNCT_1:49

.= ((f | (A `)) . x) - ((g | (A `)) . x) by A11, FUNCT_1:49

.= 0 by A3 ;

(((X --> 0) | E) | (A `)) . x = ((X --> 0) | E) . x by A11, FUNCT_1:49

.= (X --> 0) . x by A10, FUNCT_1:49 ;

hence ((f - g) | (A `)) . x = (((X --> 0) | E) | (A `)) . x by A12; :: thesis: verum

end;assume A9: x in dom ((f - g) | (A `)) ; :: thesis: ((f - g) | (A `)) . x = (((X --> 0) | E) | (A `)) . x

then A10: x in E by A7, A1, A6, XBOOLE_0:def 4;

A11: ( x in dom (f - g) & x in A ` ) by A5, A9, XBOOLE_0:def 4;

then A12: ((f - g) | (A `)) . x = (f - g) . x by FUNCT_1:49

.= (f . x) - (g . x) by A11, VALUED_1:13

.= ((f | (A `)) . x) - (g . x) by A11, FUNCT_1:49

.= ((f | (A `)) . x) - ((g | (A `)) . x) by A11, FUNCT_1:49

.= 0 by A3 ;

(((X --> 0) | E) | (A `)) . x = ((X --> 0) | E) . x by A11, FUNCT_1:49

.= (X --> 0) . x by A10, FUNCT_1:49 ;

hence ((f - g) | (A `)) . x = (((X --> 0) | E) | (A `)) . x by A12; :: thesis: verum