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 ;
(dom f) /\ (dom g) = E by ;
then A4: ( dom (f | E) = E & dom (g | E) = E ) by ;
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
.= (f . x) - (g . x) by ;
A8: (((X --> 0) | E) | (A `)) . x = ((X --> 0) | E) . x by
.= (X --> 0) . x by
.= 0 ;
((f | E) | (A `)) . x = (f | E) . x by
.= g . x by A6, A8, A3, A7, A4, FUNCT_1:49
.= (g | E) . x by ;
hence ((f | E) | (A `)) . x = ((g | E) | (A `)) . x by ; :: thesis: verum
end;
hence f | E a.e.= g | E,M by ; :: thesis: verum