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