reconsider s = 1 as Element of REAL by XREAL_0:def 1;
#Z 0 = REAL --> s
proof
let r be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: (#Z 0) . r = (REAL --> s) . r
thus (#Z 0) . r = r #Z 0 by TAYLOR_1:def 1
.= s by PREPOWER:34
.= (REAL --> s) . r ; :: thesis: verum
end;
hence #Z 0 = REAL --> 1 ; :: thesis: verum