let r, x0, x1 be Real; for f being Function of REAL,REAL holds [!(r (#) f),x0,x1!] = r * [!f,x0,x1!]
let f be Function of REAL,REAL; [!(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!]
; verum