let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL
for c being Real st 0 <= c 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 0 <= c holds
( max+ ((- c) (#) f) = c (#) (max- f) & max- ((- c) (#) f) = c (#) (max+ f) )
let c be Real; :: thesis: ( 0 <= c implies ( max+ ((- c) (#) f) = c (#) (max- f) & max- ((- c) (#) f) = c (#) (max+ f) ) )
assume A1: 0 <= c ; :: 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;
then dom (max+ ((- c) (#) f)) = dom f by MESFUNC1:def 6;
then A3: dom (max+ ((- c) (#) f)) = dom (max- f) by MESFUNC2:def 3;
then A4: dom (max+ ((- c) (#) f)) = 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 A5: x in dom (max+ ((- c) (#) f)) ; :: thesis: (max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x
then A6: (max+ ((- c) (#) f)) . x = max ((((- c) (#) f) . x),0) by MESFUNC2:def 2
.= max (((- c) * (f . x)),0) by A2, A5, MESFUNC1:def 6
.= max ((- (c * (f . x))),0) by XXREAL_3:92 ;
(c (#) (max- f)) . x = c * ((max- f) . x) by A4, A5, MESFUNC1:def 6
.= c * (max ((- (f . x)),0)) by A3, A5, MESFUNC2:def 3
.= max ((c * (- (f . x))),(c * 0)) by A1, Th6
.= max ((- (c * (f . x))),(c * 0)) by XXREAL_3:92 ;
hence (max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x by A6; :: thesis: verum

end;

hence max+ ((- c) (#) f) = c (#) (max- f) by A4, PARTFUN1:5; :: thesis: max- ((- c) (#) f) = c (#) (max+ f)
A7: dom (max- ((- c) (#) f)) = dom ((- c) (#) f) by MESFUNC2:def 3;
then dom (max- ((- c) (#) f)) = dom f by MESFUNC1:def 6;
then A8: dom (max- ((- c) (#) f)) = dom (max+ f) by MESFUNC2:def 2;
then A9: dom (max- ((- c) (#) f)) = 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 A10: x in dom (max- ((- c) (#) f)) ; :: thesis: (max- ((- c) (#) f)) . x = (c (#) (max+ f)) . x
then A11: (max- ((- c) (#) f)) . x = max ((- (((- c) (#) f) . x)),0) by MESFUNC2:def 3
.= max ((- ((- c) * (f . x))),0) by A7, A10, MESFUNC1:def 6
.= max (((- (- c)) * (f . x)),0) by XXREAL_3:92 ;
(c (#) (max+ f)) . x = c * ((max+ f) . x) by A9, A10, MESFUNC1:def 6
.= c * (max ((f . x),0)) by A8, A10, MESFUNC2:def 2
.= max ((c * (f . x)),(c * 0)) by A1, Th6 ;
hence (max- ((- c) (#) f)) . x = (c (#) (max+ f)) . x by A11; :: thesis: verum

end;

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