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: - (R_EAL c) = - c by SUPINF_2:2;
A3: dom (max+ ((- c) (#) f)) = dom ((- c) (#) f) by MESFUNC2:def 2;
then dom (max+ ((- c) (#) f)) = dom f by MESFUNC1:def 6;
then A4: dom (max+ ((- c) (#) f)) = dom (max- f) by MESFUNC2:def 3;
then A5: 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 A6: x in dom (max+ ((- c) (#) f)) ; :: thesis: (max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x
then A7: (max+ ((- c) (#) f)) . x = max ((((- c) (#) f) . x),0) by MESFUNC2:def 2
.= max (((R_EAL (- c)) * (f . x)),0) by A3, A6, MESFUNC1:def 6
.= max ((- ((R_EAL c) * (f . x))),0) by A2, XXREAL_3:92 ;
(c (#) (max- f)) . x = (R_EAL c) * ((max- f) . x) by A5, A6, MESFUNC1:def 6
.= (R_EAL c) * (max ((- (f . x)),(R_EAL 0))) by A4, A6, MESFUNC2:def 3
.= max (((R_EAL c) * (- (f . x))),((R_EAL c) * (R_EAL 0))) by A1, Th11
.= max ((- ((R_EAL c) * (f . x))),(c * 0)) by XXREAL_3:92 ;
hence (max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x by A7; :: thesis: verum

end;

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

end;

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