set f = id REAL;
reconsider z = 1 as Element of REAL by XREAL_0:def 1;
(id REAL) `| = REAL --> z

proof

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

end;

hence (id REAL) `| = REAL --> 1 ; :: thesis: verum