let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL holds
( f a.e.= g,M iff ( max+ f a.e.= max+ g,M & max- f a.e.= max- g,M ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL holds
( f a.e.= g,M iff ( max+ f a.e.= max+ g,M & max- f a.e.= max- g,M ) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL holds
( f a.e.= g,M iff ( max+ f a.e.= max+ g,M & max- f a.e.= max- g,M ) )
let f, g be PartFunc of X,REAL; :: thesis: ( f a.e.= g,M iff ( max+ f a.e.= max+ g,M & max- f a.e.= max- g,M ) )

hereby :: thesis: ( max+ f a.e.= max+ g,M & max- f a.e.= max- g,M implies f a.e.= g,M )

assume f a.e.= g,M ; :: thesis: ( max+ f a.e.= max+ g,M & max- f a.e.= max- g,M )
then consider E being Element of S such that
A1: ( M . E = 0 & f | (E `) = g | (E `) ) by LPSPACE1:def 10;
(max+ f) | (E `) = max+ (f | (E `)) by RFUNCT_3:44;
then (max+ f) | (E `) = (max+ g) | (E `) by A1, RFUNCT_3:44;
hence max+ f a.e.= max+ g,M by A1, LPSPACE1:def 10; :: thesis: max- f a.e.= max- g,M
(max- f) | (E `) = max- (f | (E `)) by RFUNCT_3:45;
then (max- f) | (E `) = (max- g) | (E `) by A1, RFUNCT_3:45;
hence max- f a.e.= max- g,M by A1, LPSPACE1:def 10; :: thesis: verum

end;

assume that
A2: max+ f a.e.= max+ g,M and
A3: max- f a.e.= max- g,M ; :: thesis: f a.e.= g,M
consider E1 being Element of S such that
A4: ( M . E1 = 0 & (max+ f) | (E1 `) = (max+ g) | (E1 `) ) by A2, LPSPACE1:def 10;
consider E2 being Element of S such that
A5: ( M . E2 = 0 & (max- f) | (E2 `) = (max- g) | (E2 `) ) by A3, LPSPACE1:def 10;
set E = E1 \/ E2;
M . (E1 \/ E2) <= (M . E1) + (M . E2) by MEASURE1:10;
then M . (E1 \/ E2) <= 0 + 0 by A4, A5;
then A6: M . (E1 \/ E2) = 0 by SUPINF_2:51;
(max+ f) | ((E1 \/ E2) `) = ((max+ g) | (E1 `)) | ((E1 \/ E2) `) by A4, SUBSET_1:21, RELAT_1:74;
then A7: (max+ f) | ((E1 \/ E2) `) = (max+ g) | ((E1 \/ E2) `) by SUBSET_1:21, RELAT_1:74;
(max- f) | ((E1 \/ E2) `) = ((max- g) | (E2 `)) | ((E1 \/ E2) `) by A5, SUBSET_1:21, RELAT_1:74;
then A8: (max- f) | ((E1 \/ E2) `) = (max- g) | ((E1 \/ E2) `) by SUBSET_1:21, RELAT_1:74;
A9: ( dom ((max+ f) - (max- f)) = dom f & dom ((max+ g) - (max- g)) = dom g ) by RFUNCT_3:34;
dom (f | ((E1 \/ E2) `)) = dom (max+ (f | ((E1 \/ E2) `))) by RFUNCT_3:def 10;
then dom (f | ((E1 \/ E2) `)) = dom ((max+ f) | ((E1 \/ E2) `)) by RFUNCT_3:44;
then dom (f | ((E1 \/ E2) `)) = dom (max+ (g | ((E1 \/ E2) `))) by A7, RFUNCT_3:44;
then A10: dom (f | ((E1 \/ E2) `)) = dom (g | ((E1 \/ E2) `)) by RFUNCT_3:def 10;
for x being Element of X st x in dom (f | ((E1 \/ E2) `)) holds
(f | ((E1 \/ E2) `)) . x = (g | ((E1 \/ E2) `)) . x

proof

let x be Element of X; :: thesis: ( x in dom (f | ((E1 \/ E2) `)) implies (f | ((E1 \/ E2) `)) . x = (g | ((E1 \/ E2) `)) . x )
assume A11: x in dom (f | ((E1 \/ E2) `)) ; :: thesis: (f | ((E1 \/ E2) `)) . x = (g | ((E1 \/ E2) `)) . x
then A12: ( x in dom f & x in (E1 \/ E2) ` ) by RELAT_1:57;
A13: ( x in dom g & x in (E1 \/ E2) ` ) by A10, A11, RELAT_1:57;
(f | ((E1 \/ E2) `)) . x = f . x by A11, FUNCT_1:47;
then (f | ((E1 \/ E2) `)) . x = ((max+ f) - (max- f)) . x by RFUNCT_3:34;
then (f | ((E1 \/ E2) `)) . x = ((max+ f) . x) - ((max- f) . x) by A12, A9, VALUED_1:13;
then (f | ((E1 \/ E2) `)) . x = (((max+ f) | ((E1 \/ E2) `)) . x) - ((max- f) . x) by A12, FUNCT_1:49;
then (f | ((E1 \/ E2) `)) . x = (((max+ f) | ((E1 \/ E2) `)) . x) - (((max- f) | ((E1 \/ E2) `)) . x) by A12, FUNCT_1:49;
then (f | ((E1 \/ E2) `)) . x = ((max+ g) . x) - (((max- g) | ((E1 \/ E2) `)) . x) by A12, A7, A8, FUNCT_1:49;
then (f | ((E1 \/ E2) `)) . x = ((max+ g) . x) - ((max- g) . x) by A12, FUNCT_1:49;
then (f | ((E1 \/ E2) `)) . x = ((max+ g) - (max- g)) . x by A13, A9, VALUED_1:13;
then (f | ((E1 \/ E2) `)) . x = g . x by RFUNCT_3:34;
hence (f | ((E1 \/ E2) `)) . x = (g | ((E1 \/ E2) `)) . x by A13, FUNCT_1:49; :: thesis: verum

end;

hence f a.e.= g,M by A6, A10, PARTFUN1:5, LPSPACE1:def 10; :: thesis: verum