let i be Element of NAT ; :: thesis: for f being PartFunc of (REAL i),REAL
for r being Real holds <>* (r (#) f) = r (#) (<>* f)
let f be PartFunc of (REAL i),REAL; :: thesis: for r being Real holds <>* (r (#) f) = r (#) (<>* f)
let r be Real; :: thesis: <>* (r (#) f) = r (#) (<>* f)
A1: dom (<>* (r (#) f)) = dom (r (#) f) by Th3;
then A2: dom (<>* (r (#) f)) = dom f by VALUED_1:def 5;
then A3: dom (<>* (r (#) f)) = dom (<>* f) by Th3
.= dom (r (#) (<>* f)) by VALUED_2:def 39 ;

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

let x be object ; :: thesis: ( x in dom (<>* (r (#) f)) implies (<>* (r (#) f)) . x = (r (#) (<>* f)) . x )
reconsider fx = f . x as Element of REAL by XREAL_0:def 1;
assume A4: x in dom (<>* (r (#) f)) ; :: thesis: (<>* (r (#) f)) . x = (r (#) (<>* f)) . x
then (<>* (r (#) f)) . x = <*((r (#) f) . x)*> by A1, Th6
.= <*(r * (f . x))*> by A4, A1, VALUED_1:def 5
.= r (#) <*fx*> by RVSUM_1:47
.= r (#) ((<>* f) . x) by A4, A2, Th6 ;
hence (<>* (r (#) f)) . x = (r (#) (<>* f)) . x by A4, A3, VALUED_2:def 39; :: thesis: verum

end;

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