let X be non empty set ; :: thesis: for A being set holds max+ (chi (A,X)) = chi (A,X)
let A be set ; :: thesis: max+ (chi (A,X)) = chi (A,X)
A1: dom (max+ (chi (A,X))) = dom (chi (A,X)) by MESFUNC2:def 2;

now :: thesis: for x being Element of X st x in dom (max+ (chi (A,X))) holds
(max+ (chi (A,X))) . x = (chi (A,X)) . x

let x be Element of X; :: thesis: ( 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))) ; :: thesis: (max+ (chi (A,X))) . x = (chi (A,X)) . x
then 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; :: thesis: verum

end;

hence max+ (chi (A,X)) = chi (A,X) by A1, PARTFUN1:5; :: thesis: verum