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

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 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;

hence f - g a.e.= (X --> 0) | E,M by A3, A7, A1, A6, A8, PARTFUN1:5, LPSPACE1:def 10; :: thesis: verum