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:3;
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:103 ;
(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:103 ;
hence (max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x by A7; :: thesis: verum

end;

hence max+ ((- c) (#) f) = c (#) (max- f) by A5, PARTFUN1:34; :: 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:103 ;
(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:34; :: thesis: verum