consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1;
consider L being LinearFunc of F, R being RestFunc of F 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 Point of F such that
A5: for p being Real holds L /. p = p * r by Def2;
take r ; :: thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F 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 = 1 * r by A5
.= r by RLVECT_1:def 8 ;
hence ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F 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