let X be non empty set ; :: thesis: for A being set holds
( chi (+infty,A,X) = Xchi (A,X) & chi (-infty,A,X) = - (Xchi (A,X)) )
let A be set ; :: thesis: ( chi (+infty,A,X) = Xchi (A,X) & chi (-infty,A,X) = - (Xchi (A,X)) )
for x being Element of X holds (chi (+infty,A,X)) . x = (Xchi (A,X)) . x

proof

let x be Element of X; :: thesis: (chi (+infty,A,X)) . x = (Xchi (A,X)) . x

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: (chi (+infty,A,X)) . x = (Xchi (A,X)) . x

then ( (chi (+infty,A,X)) . x = +infty & (Xchi (A,X)) . x = +infty ) by Def1, MEASUR10:def 7;
hence (chi (+infty,A,X)) . x = (Xchi (A,X)) . x ; :: thesis: verum

end;

suppose not x in A ; :: thesis: (chi (+infty,A,X)) . x = (Xchi (A,X)) . x

then ( (chi (+infty,A,X)) . x = 0 & (Xchi (A,X)) . x = 0 ) by Def1, MEASUR10:def 7;
hence (chi (+infty,A,X)) . x = (Xchi (A,X)) . x ; :: thesis: verum

end;

end;

end;

hence chi (+infty,A,X) = Xchi (A,X) by FUNCT_2:def 8; :: thesis: chi (-infty,A,X) = - (Xchi (A,X))
for x being Element of X holds (chi (-infty,A,X)) . x = (- (Xchi (A,X))) . x

proof

let x be Element of X; :: thesis: (chi (-infty,A,X)) . x = (- (Xchi (A,X))) . x
x in X ;
then A1: x in dom (- (Xchi (A,X))) by FUNCT_2:def 1;
then A2: (- (Xchi (A,X))) . x = - ((Xchi (A,X)) . x) by MESFUNC1:def 7;

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: (chi (-infty,A,X)) . x = (- (Xchi (A,X))) . x

then ( (chi (-infty,A,X)) . x = -infty & (Xchi (A,X)) . x = +infty ) by Def1, MEASUR10:def 7;
hence (chi (-infty,A,X)) . x = (- (Xchi (A,X))) . x by A1, XXREAL_3:6, MESFUNC1:def 7; :: thesis: verum

end;

suppose not x in A ; :: thesis: (chi (-infty,A,X)) . x = (- (Xchi (A,X))) . x

then ( (chi (-infty,A,X)) . x = 0 & (Xchi (A,X)) . x = 0 ) by Def1, MEASUR10:def 7;
hence (chi (-infty,A,X)) . x = (- (Xchi (A,X))) . x by A2; :: thesis: verum

end;

end;

end;

hence chi (-infty,A,X) = - (Xchi (A,X)) by FUNCT_2:def 8; :: thesis: verum