let X be non empty set ; for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st A c= (dom f) /\ (dom g) & f is A -measurable & g is A -measurable holds
(max- (f + g)) + (max+ f) is A -measurable
let S be SigmaField of X; for f, g being PartFunc of X,REAL
for A being Element of S st A c= (dom f) /\ (dom g) & f is A -measurable & g is A -measurable holds
(max- (f + g)) + (max+ f) is A -measurable
let f, g be PartFunc of X,REAL; for A being Element of S st A c= (dom f) /\ (dom g) & f is A -measurable & g is A -measurable holds
(max- (f + g)) + (max+ f) is A -measurable
let A be Element of S; ( A c= (dom f) /\ (dom g) & f is A -measurable & g is A -measurable implies (max- (f + g)) + (max+ f) is A -measurable )
assume that
A1:
A c= (dom f) /\ (dom g)
and
A2:
f is A -measurable
and
A3:
g is A -measurable
; (max- (f + g)) + (max+ f) is A -measurable
A4:
max+ f is A -measurable
by A2, Th46;
A5:
dom (f + g) = (dom f) /\ (dom g)
by VALUED_1:def 1;
f + g is A -measurable
by A2, A3, Th26;
then
max- (f + g) is A -measurable
by A1, A5, Th47;
hence
(max- (f + g)) + (max+ f) is A -measurable
by A4, Th26; verum