consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: ex L being LINEAR ex R being REST st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A1, Def5;
consider L being LINEAR, R being REST such that
A4: for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;
consider r being Real such that
A5: for p being Real holds L . p = r * p by Def4;
take r ; :: thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
L . 1 = r * 1 by A5
.= r ;
hence ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A2, A4; :: thesis: verum