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
.= 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 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 2;
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 ;
(c (#) (max+ f)) . x = c * ((max+ f) . x) by A2, A3, MESFUNC1:def 6
.= c * (max ((f . x),0)) by A5, MESFUNC2:def 2
.= max ((c * (f . x)),(c * 0)) by A1, Th6 ;
hence (max+ (c (#) f)) . x = (c (#) (max+ f)) . x by A6; :: thesis: verum

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 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 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 3;
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 ;
(c (#) (max- f)) . x = c * ((max- f) . x) by A7, A8, MESFUNC1:def 6
.= c * (max ((- (f . x)),0)) by A10, 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 A11; :: thesis: verum

end;

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