let r be Real; :: thesis: for f being differentiable Function of REAL,REAL holds (f - r) `| = f `|
let f be differentiable Function of REAL,REAL; :: thesis: (f - r) `| = f `|
reconsider s = r as Element of REAL by XREAL_0:def 1;
set g = REAL --> s;
A1: (REAL --> s) `| = REAL --> 0 by Th11;
A2: dom (f `|) = REAL by FUNCT_2:def 1;
dom f = REAL by FUNCT_2:def 1;
then f - r = f - (REAL --> s) by Th4;
hence (f - r) `| = (f `|) - ((REAL --> s) `|) by Th15
.= f `| by A1, A2, Th7 ;
:: thesis: verum