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

[!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