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!]
x1 in REAL by XREAL_0:def 1;
then A1: x1 in dom (r (#) f) by FUNCT_2:def 1;
x0 in REAL by XREAL_0:def 1;
then x0 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:74 ;
hence [!(r (#) f),x0,x1!] = r * [!f,x0,x1!] ; :: thesis: verum