let X be non empty set ; for A being set holds max+ (chi (A,X)) = chi (A,X)
let A be set ; max+ (chi (A,X)) = chi (A,X)
A1:
dom (max+ (chi (A,X))) = dom (chi (A,X))
by MESFUNC2:def 2;
now for x being Element of X st x in dom (max+ (chi (A,X))) holds
(max+ (chi (A,X))) . x = (chi (A,X)) . xlet x be
Element of
X;
( x in dom (max+ (chi (A,X))) implies (max+ (chi (A,X))) . x = (chi (A,X)) . x )A2:
rng (chi (A,X)) c= {0,1}
by FUNCT_3:39;
assume A3:
x in dom (max+ (chi (A,X)))
;
(max+ (chi (A,X))) . x = (chi (A,X)) . xthen A4:
(max+ (chi (A,X))) . x = max (
((chi (A,X)) . x),
0.)
by MESFUNC2:def 2;
(chi (A,X)) . x in rng (chi (A,X))
by A1, A3, FUNCT_1:3;
hence
(max+ (chi (A,X))) . x = (chi (A,X)) . x
by A4, A2, XXREAL_0:def 10;
verum end;
hence
max+ (chi (A,X)) = chi (A,X)
by A1, PARTFUN1:5; verum