let f be Function of R^1 ,R^1 ; :: thesis:
given a, b being Real such that A1: for x being Real holds f . x = (a * x) + b ; :: thesis:
for W being Point of R^1
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G

proof

let W be Point of R^1 ; :: thesis:
let G be a_neighborhood of f . W; :: thesis:
A2: f . W in Int G by CONNSP_2:def 1;
then consider Q being Subset of R^1 such that
A3: ( Q is open & Q c= G & f . W in Q ) by TOPS_1:54;
reconsider Y = f . W as Point of RealSpace by Th24, METRIC_1:def 14;
consider r being real number such that
A4: ( r > 0 & Ball Y,r c= Q ) by A3, Th22;

now

per cases ;

suppose A5: a = 0 ; :: thesis:

set H = [#] R^1 ;
( [#] R^1 is open & W in [#] R^1 ) ;
then W in Int ([#] R^1 ) by TOPS_1:55;
then reconsider H = [#] R^1 as a_neighborhood of W by CONNSP_2:def 1;
for y being set holds
( y in {b} iff ex x being set st
( x in dom f & x in H & y = f . x ) )

proof

let y be set ; :: thesis:
thus ( y in {b} implies ex x being set st
( x in dom f & x in H & y = f . x ) ) :: thesis:

proof

assume A6: y in {b} ; :: thesis:
take 0 ; :: thesis:
( dom f = the carrier of R^1 & the carrier of R^1 = [#] R^1 & the carrier of R^1 = REAL ) by Th24, FUNCT_2:def 1;
hence ( 0 in dom f & 0 in H ) ; :: thesis:
thus f . 0 = (0 * 0 ) + b by A1, A5
.= y by A6, TARSKI:def 1 ; :: thesis:

end;

given x being set such that A7: ( x in dom f & x in H & y = f . x ) ; :: thesis:
reconsider x = x as Real by A7, Th24;
y = (0 * x) + b by A1, A5, A7
.= b ;
hence y in {b} by TARSKI:def 1; :: thesis:

end;

then A8: f .: H = {b} by FUNCT_1:def 12;
A9: Int G c= G by TOPS_1:44;
reconsider W' = W as Real by Th24;
f . W = (0 * W') + b by A1, A5
.= b ;
then f .: H c= G by A2, A8, A9, ZFMISC_1:37;
hence ex H being a_neighborhood of W st f .: H c= G ; :: thesis:

end;

suppose A10: a <> 0 ; :: thesis:

set d = r / (2 * (abs a));
( abs a > 0 & 2 > 0 ) by A10, COMPLEX1:133;
then 2 * (abs a) > 0 by XREAL_1:131;
then A11: r / (2 * (abs a)) > 0 by A4, XREAL_1:141;
reconsider W' = W as Point of RealSpace by Th24, METRIC_1:def 14;
reconsider H = Ball W',(r / (2 * (abs a))) as Subset of R^1 by Th24, METRIC_1:def 14;
H is open by Th21;
then Int H = H by TOPS_1:55;
then W in Int H by A11, TBSP_1:16;
then reconsider H = H as a_neighborhood of W by CONNSP_2:def 1;
A12: f .: H c= Ball Y,r

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in f .: H ; :: thesis:
then consider x being set such that
A13: ( x in dom f & x in H & y = f . x ) by FUNCT_1:def 12;
reconsider y' = y as Real by A13, Th24, FUNCT_2:7;
reconsider x' = x as Point of RealSpace by A13;
reconsider Y' = Y as Real by METRIC_1:def 14;
reconsider W'' = W' as Real by Th24;
reconsider x'' = x' as Real by METRIC_1:def 14;
dist W',x' < r / (2 * (abs a)) by A13, METRIC_1:12;
then ( abs (W'' - x'') < r / (2 * (abs a)) & abs a > 0 ) by A10, Th15, COMPLEX1:133;
then (abs a) * (abs (W'' - x'')) < (abs a) * (r / (2 * (abs a))) by XREAL_1:70;
then abs (a * (W'' - x'')) < (abs a) * (r / (2 * (abs a))) by COMPLEX1:151;
then abs (((a * W'') + b) - ((a * x'') + b)) < (abs a) * (r / (2 * (abs a))) ;
then abs (Y' - ((a * x'') + b)) < (abs a) * (r / (2 * (abs a))) by A1;
then A14: abs (Y' - y') < (abs a) * (r / (2 * (abs a))) by A1, A13;
( abs a <> 0 & 2 <> 0 ) by A10, ABSVALUE:7;
then A15: (abs a) * (r / (2 * (abs a))) = r / 2 by XCMPLX_1:93;
reconsider yy = y' as Point of RealSpace by METRIC_1:def 14;
( (r / 2) + (r / 2) = r & r / 2 >= 0 ) by A4, XREAL_1:138;
then abs (Y' - y') < r by A14, A15, Lm2;
then dist Y,yy < r by Th15;
hence y in Ball Y,r by METRIC_1:12; :: thesis:

end;

Ball Y,r c= G by A3, A4, XBOOLE_1:1;
hence ex H being a_neighborhood of W st f .: H c= G by A12, XBOOLE_1:1; :: thesis:

end;

hence ex H being a_neighborhood of W st f .: H c= G ; :: thesis:

end;

hence f is continuous by BORSUK_1:def 3; :: thesis: