ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) ) by A1, Def3;
hence ex b₁ being Point of T ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - b₁).|| < e ) ) ) ) ; :: thesis: verum