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