let i be Element of NAT ; :: thesis: for f being PartFunc of (REAL i),REAL
for r being real number holds <>* (r (#) f) = r (#) (<>* f)
let f be PartFunc of (REAL i),REAL; :: thesis: for r being real number holds <>* (r (#) f) = r (#) (<>* f)
let r be real number ; :: thesis: <>* (r (#) f) = r (#) (<>* f)
P1: dom (<>* (r (#) f)) = dom (r (#) f) by LMXTh0;
then P2: dom (<>* (r (#) f)) = dom f by VALUED_1:def 5;
then P4: dom (<>* (r (#) f)) = dom (<>* f) by LMXTh0
.= dom (r (#) (<>* f)) by VALUED_2:def 39 ;

now :: thesis: for x being set st x in dom (<>* (r (#) f)) holds
(<>* (r (#) f)) . x = (r (#) (<>* f)) . x

let x be set ; :: thesis: ( x in dom (<>* (r (#) f)) implies (<>* (r (#) f)) . x = (r (#) (<>* f)) . x )
assume A0: x in dom (<>* (r (#) f)) ; :: thesis: (<>* (r (#) f)) . x = (r (#) (<>* f)) . x
then (<>* (r (#) f)) . x = <*((r (#) f) . x)*> by P1, XTh30
.= <*(r * (f . x))*> by A0, P1, VALUED_1:def 5
.= r (#) <*(f . x)*> by RVSUM_1:47
.= r (#) ((<>* f) . x) by A0, P2, XTh30 ;
hence (<>* (r (#) f)) . x = (r (#) (<>* f)) . x by A0, P4, VALUED_2:def 39; :: thesis: verum

end;

hence <>* (r (#) f) = r (#) (<>* f) by P4, FUNCT_1:2; :: thesis: verum