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

end;

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

end;

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