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 )
assume A1: f is constant ; :: thesis: [!f,x0,x1!] = 0
( x0 in REAL & x1 in REAL ) ;
then ( x0 in dom f & x1 in dom f ) by FUNCT_2:def 1;
then f . x0 = f . x1 by A1, FUNCT_1:def 16;
hence [!f,x0,x1!] = 0 ; :: thesis: verum