consider N being Neighbourhood of x0 such that

A2: N c= dom f and

A3: ex L being LinearFunc ex R being RestFunc 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, R being RestFunc 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 Def3;

take r ; :: thesis: ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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

A2: N c= dom f and

A3: ex L being LinearFunc ex R being RestFunc 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, R being RestFunc 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 Def3;

take r ; :: thesis: ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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