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