let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL
for c being Real st c <= 0 holds
( max+ (c (#) f) = (- c) (#) (max- f) & max- (c (#) f) = (- c) (#) (max+ f) )
let f be PartFunc of C,ExtREAL; :: thesis: for c being Real st c <= 0 holds
( max+ (c (#) f) = (- c) (#) (max- f) & max- (c (#) f) = (- c) (#) (max+ f) )
let c be Real; :: thesis: ( c <= 0 implies ( max+ (c (#) f) = (- c) (#) (max- f) & max- (c (#) f) = (- c) (#) (max+ f) ) )
assume A1: c <= 0 ; :: thesis: ( max+ (c (#) f) = (- c) (#) (max- f) & max- (c (#) f) = (- c) (#) (max+ f) )
A2: dom (max+ (c (#) f)) = dom (c (#) f) by MESFUNC2:def 2
.= dom f by MESFUNC1:def 6
.= dom (max- f) by MESFUNC2:def 3
.= dom ((- c) (#) (max- f)) by MESFUNC1:def 6 ;
for x being Element of C st x in dom (max+ (c (#) f)) holds
(max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x

proof

let x be Element of C; :: thesis: ( x in dom (max+ (c (#) f)) implies (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x )
assume A3: x in dom (max+ (c (#) f)) ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x
then A4: x in dom (c (#) f) by MESFUNC2:def 2;
then x in dom f by MESFUNC1:def 6;
then A5: x in dom (max- f) by MESFUNC2:def 3;
A6: (max+ (c (#) f)) . x = max (((c (#) f) . x),0) by A3, MESFUNC2:def 2
.= max ((c * (f . x)),0) by A4, MESFUNC1:def 6 ;
B1: ((- c) (#) (max- f)) . x = (- c) * ((max- f) . x) by A2, A3, MESFUNC1:def 6
.= (- c) * (max ((- (f . x)),0)) by A5, MESFUNC2:def 3 ;

per cases ( f . x >= 0 or f . x < 0 ) ;

suppose f . x >= 0 ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x

then ( (max+ (c (#) f)) . x = 0 & max ((- (f . x)),0) = 0 ) by A1, A6, XXREAL_0:def 10;
hence (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x by B1; :: thesis: verum

end;

suppose D1: f . x < 0 ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x

then B2: ( (max+ (c (#) f)) . x = c * (f . x) & max ((- (f . x)),0) = - (f . x) ) by A1, A6, XXREAL_0:def 10;

per cases ( f . x = -infty or f . x in REAL ) by D1, XXREAL_0:14;

suppose E1: f . x = -infty ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x

per cases ( c = 0 or c < 0 ) by A1;

suppose c = 0 ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x

then ( (max+ (c (#) f)) . x = 0 & ((- c) (#) (max- f)) . x = 0 ) by B1, A6, XXREAL_0:def 10;
hence (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x ; :: thesis: verum

end;

suppose F1: c < 0 ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x

then (- c) * (- (f . x)) = +infty by E1, XXREAL_3:5, XXREAL_3:def 5;
hence (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x by B1, B2, E1, F1, XXREAL_3:def 5; :: thesis: verum

end;

end;

end;

suppose f . x in REAL ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x

then reconsider a = f . x as Real ;
(- c) * (- a) = (- c) * (- (f . x)) ;
then (- c) * (- (f . x)) = c * a
.= c * (f . x) ;
hence (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x by B1, B2; :: thesis: verum

end;

end;

end;

end;

end;

hence max+ (c (#) f) = (- c) (#) (max- f) by A2, PARTFUN1:5; :: thesis: max- (c (#) f) = (- c) (#) (max+ f)
A7: dom (max- (c (#) f)) = dom (c (#) f) by MESFUNC2:def 3
.= dom f by MESFUNC1:def 6
.= dom (max+ f) by MESFUNC2:def 2
.= dom ((- c) (#) (max+ f)) by MESFUNC1:def 6 ;
for x being Element of C st x in dom (max- (c (#) f)) holds
(max- (c (#) f)) . x = ((- c) (#) (max+ f)) . x

proof

let x be Element of C; :: thesis: ( x in dom (max- (c (#) f)) implies (max- (c (#) f)) . x = ((- c) (#) (max+ f)) . x )
assume A8: x in dom (max- (c (#) f)) ; :: thesis: (max- (c (#) f)) . x = ((- c) (#) (max+ f)) . x
then A9: x in dom (c (#) f) by MESFUNC2:def 3;
then x in dom f by MESFUNC1:def 6;
then A10: x in dom (max+ f) by MESFUNC2:def 2;
A11: (max- (c (#) f)) . x = max ((- ((c (#) f) . x)),0) by A8, MESFUNC2:def 3
.= max ((- (c * (f . x))),0) by A9, MESFUNC1:def 6 ;
A12: ((- c) (#) (max+ f)) . x = (- c) * ((max+ f) . x) by A7, A8, MESFUNC1:def 6
.= (- c) * (max ((f . x),0)) by A10, MESFUNC2:def 2
.= max (((- c) * (f . x)),((- c) * 0)) by A1, MESFUNC5:6
.= max (((- c) * (f . x)),0) ;
- (c * (f . x)) = (- c) * (f . x)

proof

per cases ( f . x = +infty or f . x = -infty or f . x in REAL ) by XXREAL_0:14;

suppose E1: f . x = +infty ; :: thesis: - (c * (f . x)) = (- c) * (f . x)

per cases ( c = 0 or c < 0 ) by A1;

suppose c = 0 ; :: thesis: - (c * (f . x)) = (- c) * (f . x)

then ( c * (f . x) = 0 & (- c) * (f . x) = 0 ) ;
hence - (c * (f . x)) = (- c) * (f . x) ; :: thesis: verum

end;

suppose E2: c < 0 ; :: thesis: - (c * (f . x)) = (- c) * (f . x)

then c * (f . x) = -infty by E1, XXREAL_3:def 5;
hence - (c * (f . x)) = (- c) * (f . x) by E1, E2, XXREAL_3:5, XXREAL_3:def 5; :: thesis: verum

end;

end;

end;

suppose E1: f . x = -infty ; :: thesis: - (c * (f . x)) = (- c) * (f . x)

per cases ( c = 0 or c < 0 ) by A1;

suppose c = 0 ; :: thesis: - (c * (f . x)) = (- c) * (f . x)

then ( c * (f . x) = 0 & (- c) * (f . x) = 0 ) ;
hence - (c * (f . x)) = (- c) * (f . x) ; :: thesis: verum

end;

suppose E2: c < 0 ; :: thesis: - (c * (f . x)) = (- c) * (f . x)

then c * (f . x) = +infty by E1, XXREAL_3:def 5;
hence - (c * (f . x)) = (- c) * (f . x) by E1, E2, XXREAL_3:6, XXREAL_3:def 5; :: thesis: verum

end;

end;

end;

suppose f . x in REAL ; :: thesis: - (c * (f . x)) = (- c) * (f . x)

then reconsider a = f . x as Real ;
(- c) * a = (- c) * (f . x) ;
then (- c) * (f . x) = - (c * a) ;
hence - (c * (f . x)) = (- c) * (f . x) ; :: thesis: verum

end;

end;

end;

hence (max- (c (#) f)) . x = ((- c) (#) (max+ f)) . x by A11, A12; :: thesis: verum

end;

hence max- (c (#) f) = (- c) (#) (max+ f) by A7, PARTFUN1:5; :: thesis: verum