let X be set ; :: thesis: for A being Subset of X
for er being ExtReal holds
( ( er >= 0 implies chi (er,A,X) is nonnegative ) & ( er <= 0 implies chi (er,A,X) is nonpositive ) )
let A be Subset of X; :: thesis: for er being ExtReal holds
( ( er >= 0 implies chi (er,A,X) is nonnegative ) & ( er <= 0 implies chi (er,A,X) is nonpositive ) )
let er be ExtReal; :: thesis: ( ( er >= 0 implies chi (er,A,X) is nonnegative ) & ( er <= 0 implies chi (er,A,X) is nonpositive ) )
hereby :: thesis: ( er <= 0 implies chi (er,A,X) is nonpositive )
assume a1: er >= 0 ; :: thesis: chi (er,A,X) is nonnegative
now :: thesis: for x being object st x in dom (chi (er,A,X)) holds
(chi (er,A,X)) . x >= 0
let x be object ; :: thesis: ( x in dom (chi (er,A,X)) implies (chi (er,A,X)) . x >= 0 )
assume a2: x in dom (chi (er,A,X)) ; :: thesis: (chi (er,A,X)) . x >= 0
( x in A implies (chi (er,A,X)) . x >= 0 ) by a1, Def1;
hence (chi (er,A,X)) . x >= 0 by a2, Def1; :: thesis: verum
end;
hence chi (er,A,X) is nonnegative by SUPINF_2:52; :: thesis: verum
end;
assume a3: er <= 0 ; :: thesis: chi (er,A,X) is nonpositive
now :: thesis: for x being set st x in dom (chi (er,A,X)) holds
(chi (er,A,X)) . x <= 0
let x be set ; :: thesis: ( x in dom (chi (er,A,X)) implies (chi (er,A,X)) . x <= 0 )
assume a4: x in dom (chi (er,A,X)) ; :: thesis: (chi (er,A,X)) . x <= 0
( x in A implies (chi (er,A,X)) . x <= 0 ) by a3, Def1;
hence (chi (er,A,X)) . x <= 0 by a4, Def1; :: thesis: verum
end;
hence chi (er,A,X) is nonpositive by MESFUNC5:9; :: thesis: verum