let r be Real; :: thesis: for f being differentiable Function of REAL,REAL holds (r + f) `| = f `|
let f be differentiable Function of REAL,REAL; :: thesis: (r + f) `| = 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 r + f = (REAL --> s) + f by Th3;
hence (r + f) `| = ((REAL --> s) `|) + (f `|) by Th14
.= f `| by A1, A2, Th6 ;
:: thesis: verum