consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,T) ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def6;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators S,T), R being REST of S,T such that
A4: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3;
take L ; :: thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
thus ex N being Neighbourhood of x0 st
( N c= dom f & ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by A2, A4; :: thesis: verum