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

proof

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;

hence f | E a.e.= g | E,M by A3, A5, PARTFUN1:5, LPSPACE1:def 10; :: thesis: verum