let f be constant Function of REAL,REAL; :: thesis: f `| = REAL --> 0
reconsider z = 0 as Element of REAL by XREAL_0:def 1;
f `| = REAL --> z

proof

let r be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: (f `|) . r = (REAL --> z) . r
A1: f | REAL = f ;
dom f = REAL by FUNCT_2:def 1;
hence (f `|) . r = z by A1, Lm1, FDIFF_1:22
.= (REAL --> z) . r ;
:: thesis: verum

end;

hence f `| = REAL --> 0 ; :: thesis: verum