let C be non empty set ; :: thesis: for f being PartFunc of C,REAL holds max- f = max+ (- f)
let f be PartFunc of C,REAL; :: thesis: max- f = max+ (- f)
dom (max+ (- f)) = dom (- f) by RFUNCT_3:def 10;
then A1: dom (max+ (- f)) = dom f by VALUED_1:8;
A2: dom (max- f) = dom f by RFUNCT_3:def 11;
for x1 being Element of C st x1 in dom f holds
(max- f) . x1 = (max+ (- f)) . x1
proof
let x1 be Element of C; :: thesis: ( x1 in dom f implies (max- f) . x1 = (max+ (- f)) . x1 )
assume A3: x1 in dom f ; :: thesis: (max- f) . x1 = (max+ (- f)) . x1
then A4: (max+ (- f)) . x1 = max+ ((- f) . x1) by A1, RFUNCT_3:def 10
.= max (((- f) . x1),0) by RFUNCT_3:def 1
.= max ((- (f . x1)),0) by VALUED_1:8 ;
(max- f) . x1 = max- (f . x1) by A2, A3, RFUNCT_3:def 11
.= max ((- (f . x1)),0) by RFUNCT_3:def 2 ;
hence (max- f) . x1 = (max+ (- f)) . x1 by A4; :: thesis: verum
end;
hence max- f = max+ (- f) by A2, A1, PARTFUN1:5; :: thesis: verum