let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for r being Real st 0 <= r holds
( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) )
let f be PartFunc of X,REAL; :: thesis: for r being Real st 0 <= r holds
( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) )
let r be Real; :: thesis: ( 0 <= r implies ( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) ) )
assume A1: 0 <= r ; :: thesis: ( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) )
A2: dom (max+ ((- r) (#) f)) = dom ((- r) (#) f) by RFUNCT_3:def 10;
then dom (max+ ((- r) (#) f)) = dom f by VALUED_1:def 5;
then A3: dom (max+ ((- r) (#) f)) = dom (max- f) by RFUNCT_3:def 11;
then A4: dom (max+ ((- r) (#) f)) = dom (r (#) (max- f)) by VALUED_1:def 5;
reconsider rr = r as Real ;
for x being Element of X st x in dom (max+ ((- r) (#) f)) holds
(max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x

proof

let x be Element of X; :: thesis: ( x in dom (max+ ((- r) (#) f)) implies (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x )
assume A5: x in dom (max+ ((- r) (#) f)) ; :: thesis: (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x
then A6: (max+ ((- r) (#) f)) . x = max+ (((- r) (#) f) . x) by RFUNCT_3:def 10
.= max (((- r) * (f . x)),0) by A2, A5, VALUED_1:def 5 ;
(r (#) (max- f)) . x = r * ((max- f) . x) by A4, A5, VALUED_1:def 5
.= rr * (max- (f . x)) by A3, A5, RFUNCT_3:def 11
.= max ((rr * (- (f . x))),(rr * 0)) by A1, FUZZY_2:41 ;
hence (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x by A6; :: thesis: verum

end;

hence max+ ((- r) (#) f) = r (#) (max- f) by A4, PARTFUN1:5; :: thesis: max- ((- r) (#) f) = r (#) (max+ f)
A7: dom (max- ((- r) (#) f)) = dom ((- r) (#) f) by RFUNCT_3:def 11;
then dom (max- ((- r) (#) f)) = dom f by VALUED_1:def 5;
then A8: dom (max- ((- r) (#) f)) = dom (max+ f) by RFUNCT_3:def 10;
then A9: dom (max- ((- r) (#) f)) = dom (r (#) (max+ f)) by VALUED_1:def 5;
for x being Element of X st x in dom (max- ((- r) (#) f)) holds
(max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x

proof

let x be Element of X; :: thesis: ( x in dom (max- ((- r) (#) f)) implies (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x )
assume A10: x in dom (max- ((- r) (#) f)) ; :: thesis: (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x
then A11: (max- ((- r) (#) f)) . x = max- (((- r) (#) f) . x) by RFUNCT_3:def 11
.= max ((- ((- r) * (f . x))),0) by A7, A10, VALUED_1:def 5 ;
(r (#) (max+ f)) . x = r * ((max+ f) . x) by A9, A10, VALUED_1:def 5
.= rr * (max+ (f . x)) by A8, A10, RFUNCT_3:def 10
.= max ((rr * (f . x)),(rr * 0)) by A1, FUZZY_2:41 ;
hence (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x by A11; :: thesis: verum

end;

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