let x0, x1 be Real; :: thesis: for f being Function of REAL ,REAL holds [!f,x0,x1!] = [!f,x1,x0!]
let f be Function of REAL ,REAL ; :: thesis: [!f,x0,x1!] = [!f,x1,x0!]
thus [!f,x0,x1!] = (- ((f . x1) - (f . x0))) / (- (x1 - x0))
.= [!f,x1,x0!] by XCMPLX_1:192 ; :: thesis: verum