let r be Real; :: thesis: for f being differentiable Function of REAL,REAL holds (f `|) . r = diff (f,r)
let f be differentiable Function of REAL,REAL; :: thesis: (f `|) . r = diff (f,r)
dom f = REAL by FUNCT_2:def 1;
then A1: f is_differentiable_on REAL by FDIFF_1:def 8;
r in REAL by XREAL_0:def 1;
hence (f `|) . r = diff (f,r) by A1, FDIFF_1:def 7; :: thesis: verum