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

let x be Element of X; :: thesis: ( x in dom (max+ (chi A,X)) implies (max+ (chi A,X)) . x = (chi A,X) . x )
assume A2: x in dom (max+ (chi A,X)) ; :: thesis: (max+ (chi A,X)) . x = (chi A,X) . x
then A3: (max+ (chi A,X)) . x = max ((chi A,X) . x),0. by MESFUNC2:def 2;
A4: (chi A,X) . x in rng (chi A,X) by A1, A2, FUNCT_1:12;
rng (chi A,X) c= {0 ,1} by FUNCT_3:48;
then ( (chi A,X) . x = 0 or (chi A,X) . x = 1 ) by A4, TARSKI:def 2;
hence (max+ (chi A,X)) . x = (chi A,X) . x by A3, XXREAL_0:def 10; :: thesis: verum

end;

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