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