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 )
A2: rng (chi A,X) c= {0 ,1} by FUNCT_3:48;
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:12;
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:34; :: thesis: verum