let r, x0, x1, x2, x3, x4, x5 be Real; :: thesis: for f being Function of REAL ,REAL holds [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!]
let f be Function of REAL ,REAL ; :: thesis: [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!]
[!(r (#) f),x0,x1,x2,x3,x4,x5!] = ((r * [!f,x0,x1,x2,x3,x4!]) - [!(r (#) f),x1,x2,x3,x4,x5!]) / (x0 - x5) by Th11
.= ((r * [!f,x0,x1,x2,x3,x4!]) - (r * [!f,x1,x2,x3,x4,x5!])) / (x0 - x5) by Th11
.= (r * ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!])) / (x0 - x5) ;
hence [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!] by XCMPLX_1:75; :: thesis: verum