let x0, x1 be Real; :: thesis: for f being Function of REAL,REAL st f is constant holds
[!f,x0,x1!] = 0
let f be Function of REAL,REAL; :: thesis: ( f is constant implies [!f,x0,x1!] = 0 )
x0 in REAL by XREAL_0:def 1;
then A1: x0 in dom f by FUNCT_2:def 1;
x1 in REAL by XREAL_0:def 1;
then A2: x1 in dom f by FUNCT_2:def 1;
assume f is constant ; :: thesis: [!f,x0,x1!] = 0
then f . x0 = f . x1 by A1, A2, FUNCT_1:def 10;
hence [!f,x0,x1!] = 0 ; :: thesis: verum