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 - g) & f - g a.e.= (X --> 0) | E,M holds

f | E a.e.= g | 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 - g) & f - g a.e.= (X --> 0) | E,M holds

f | E a.e.= g | 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 - g) & f - g a.e.= (X --> 0) | E,M holds

f | E a.e.= g | E,M

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

f | E a.e.= g | E,M

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

assume that

A1: E = dom (f - g) and

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

consider A being Element of S such that

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

(dom f) /\ (dom g) = E by A1, VALUED_1:12;

then A4: ( dom (f | E) = E & dom (g | E) = E ) by XBOOLE_1:17, RELAT_1:62;

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

.= dom ((g | E) | (A `)) by RELAT_1:61 ;

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

((f | E) | (A `)) . x = ((g | 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 - g) & f - g a.e.= (X --> 0) | E,M holds

f | E a.e.= g | 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 - g) & f - g a.e.= (X --> 0) | E,M holds

f | E a.e.= g | 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 - g) & f - g a.e.= (X --> 0) | E,M holds

f | E a.e.= g | E,M

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

f | E a.e.= g | E,M

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

assume that

A1: E = dom (f - g) and

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

consider A being Element of S such that

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

(dom f) /\ (dom g) = E by A1, VALUED_1:12;

then A4: ( dom (f | E) = E & dom (g | E) = E ) by XBOOLE_1:17, RELAT_1:62;

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

.= dom ((g | E) | (A `)) by RELAT_1:61 ;

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

((f | E) | (A `)) . x = ((g | E) | (A `)) . x

proof

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

assume x in dom ((f | E) | (A `)) ; :: thesis: ((f | E) | (A `)) . x = ((g | E) | (A `)) . x

then A6: ( x in dom (f | E) & x in A ` ) by RELAT_1:57;

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

.= (f . x) - (g . x) by A1, A6, A4, VALUED_1:13 ;

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

.= (X --> 0) . x by A6, A4, FUNCT_1:49

.= 0 ;

((f | E) | (A `)) . x = (f | E) . x by A6, FUNCT_1:49

.= g . x by A6, A8, A3, A7, A4, FUNCT_1:49

.= (g | E) . x by A6, A4, FUNCT_1:49 ;

hence ((f | E) | (A `)) . x = ((g | E) | (A `)) . x by A6, FUNCT_1:49; :: thesis: verum

end;assume x in dom ((f | E) | (A `)) ; :: thesis: ((f | E) | (A `)) . x = ((g | E) | (A `)) . x

then A6: ( x in dom (f | E) & x in A ` ) by RELAT_1:57;

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

.= (f . x) - (g . x) by A1, A6, A4, VALUED_1:13 ;

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

.= (X --> 0) . x by A6, A4, FUNCT_1:49

.= 0 ;

((f | E) | (A `)) . x = (f | E) . x by A6, FUNCT_1:49

.= g . x by A6, A8, A3, A7, A4, FUNCT_1:49

.= (g | E) . x by A6, A4, FUNCT_1:49 ;

hence ((f | E) | (A `)) . x = ((g | E) | (A `)) . x by A6, FUNCT_1:49; :: thesis: verum