let x0, x1, x2 be Real; :: thesis: for f being Function of REAL,REAL st f is constant holds

[!f,x0,x1,x2!] = 0

let f be Function of REAL,REAL; :: thesis: ( f is constant implies [!f,x0,x1,x2!] = 0 )

assume A1: f is constant ; :: thesis: [!f,x0,x1,x2!] = 0

then [!f,x0,x1,x2!] = (0 - [!f,x1,x2!]) / (x0 - x2) by DIFF_1:30

.= (0 - 0) / (x0 - x2) by A1, DIFF_1:30 ;

hence [!f,x0,x1,x2!] = 0 ; :: thesis: verum

[!f,x0,x1,x2!] = 0

let f be Function of REAL,REAL; :: thesis: ( f is constant implies [!f,x0,x1,x2!] = 0 )

assume A1: f is constant ; :: thesis: [!f,x0,x1,x2!] = 0

then [!f,x0,x1,x2!] = (0 - [!f,x1,x2!]) / (x0 - x2) by DIFF_1:30

.= (0 - 0) / (x0 - x2) by A1, DIFF_1:30 ;

hence [!f,x0,x1,x2!] = 0 ; :: thesis: verum