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) & dom (max- ((- r) (#) f)) = dom ((- r) (#) f) ) by RFUNCT_3:def 10, RFUNCT_3:def 11;
then ( dom (max+ ((- r) (#) f)) = dom f & dom (max- ((- r) (#) f)) = dom f ) by VALUED_1:def 5;
then A3: ( dom (max+ ((- r) (#) f)) = dom (max- f) & dom (max- ((- r) (#) f)) = dom (max+ f) ) by RFUNCT_3:def 10, RFUNCT_3:def 11;
then A4: ( dom (max+ ((- r) (#) f)) = dom (r (#) (max- f)) & 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 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
.= r * (max- (f . x)) by A3, A5, RFUNCT_3:def 11
.= max (r * (- (f . x))),(r * 0 ) by A1, FUZZY_2:46 ;
hence (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x by A6; :: thesis: verum

end;

hence max+ ((- r) (#) f) = r (#) (max- f) by A4, PARTFUN1:34; :: thesis: max- ((- r) (#) f) = r (#) (max+ f)
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 A7: x in dom (max- ((- r) (#) f)) ; :: thesis: (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x
then A8: (max- ((- r) (#) f)) . x = max- (((- r) (#) f) . x) by RFUNCT_3:def 11
.= max (- ((- r) * (f . x))),0 by A2, A7, VALUED_1:def 5 ;
(r (#) (max+ f)) . x = r * ((max+ f) . x) by A4, A7, VALUED_1:def 5
.= r * (max+ (f . x)) by A3, A7, RFUNCT_3:def 10
.= max (r * (f . x)),(r * 0 ) by A1, FUZZY_2:46 ;
hence (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x by A8; :: thesis: verum

end;

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