let r, x0, x1 be Real; :: thesis: for f being Function of REAL ,REAL holds [!(r (#) f),x0,x1!] = r * [!f,x0,x1!]
let f be Function of REAL ,REAL ; :: thesis: [!(r (#) f),x0,x1!] = r * [!f,x0,x1!]
( x0 in REAL & x1 in REAL ) ;
then A1: ( x0 in dom (r (#) f) & x1 in dom (r (#) f) ) by FUNCT_2:def 1;
then [!(r (#) f),x0,x1!] = ((r * (f . x0)) - ((r (#) f) . x1)) / (x0 - x1) by VALUED_1:def 5
.= ((r * (f . x0)) - (r * (f . x1))) / (x0 - x1) by A1, VALUED_1:def 5
.= (r * ((f . x0) - (f . x1))) / (x0 - x1)
.= r * [!f,x0,x1!] by XCMPLX_1:75 ;
hence [!(r (#) f),x0,x1!] = r * [!f,x0,x1!] ; :: thesis: verum