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