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:191 ; :: thesis: verum