let f be Function of R^1 ,R^1 ; :: thesis: ( ex a, b being Real st
for x being Real holds f . x = (a * x) + b implies f is continuous )
given a, b being Real such that A1: for x being Real holds f . x = (a * x) + b ; :: thesis: f is continuous
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: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
let G be a_neighborhood of f . W; :: thesis: ex H being a_neighborhood of W st f .: H c= G
reconsider Y = f . W as Point of RealSpace ;
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 and
A4: Q c= G and
A5: f . W in Q by TOPS_1:54;
consider r being real number such that
A6: r > 0 and
A7: Ball Y,r c= Q by A3, A5, Th22;

now

per cases ( a = 0 or a <> 0 ) ;

suppose A8: a = 0 ; :: thesis: ex H being a_neighborhood of W st f .: H c= G

set H = [#] R^1 ;
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: ( y in {b} iff ex x being set st
( x in dom f & x in H & y = f . x ) )
thus ( y in {b} implies ex x being set st
( x in dom f & x in H & y = f . x ) ) :: thesis: ( ex x being set st
( x in dom f & x in H & y = f . x ) implies y in {b} )

proof

assume A9: y in {b} ; :: thesis: ex x being set st
( x in dom f & x in H & y = f . x )
take 0 ; :: thesis: ( 0 in dom f & 0 in H & y = f . 0 )
dom f = the carrier of R^1 by FUNCT_2:def 1;
hence ( 0 in dom f & 0 in H ) ; :: thesis: y = f . 0
thus f . 0 = (0 * 0 ) + b by A1, A8
.= y by A9, TARSKI:def 1 ; :: thesis: verum

end;

given x being set such that A10: x in dom f and
x in H and
A11: y = f . x ; :: thesis: y in {b}
reconsider x = x as Real by A10;
y = (0 * x) + b by A1, A8, A11
.= b ;
hence y in {b} by TARSKI:def 1; :: thesis: verum

end;

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

end;

suppose A14: a <> 0 ; :: thesis: ex H being a_neighborhood of W st f .: H c= G

reconsider W9 = W as Point of RealSpace ;
set d = r / (2 * (abs a));
reconsider H = Ball W9,(r / (2 * (abs a))) as Subset of R^1 ;
H is open by Th21;
then A15: Int H = H by TOPS_1:55;
abs a > 0 by A14, COMPLEX1:133;
then 2 * (abs a) > 0 by XREAL_1:131;
then W in Int H by A6, A15, TBSP_1:16, XREAL_1:141;
then reconsider H = H as a_neighborhood of W by CONNSP_2:def 1;
A16: f .: H c= Ball Y,r

proof

reconsider W99 = W9 as Real ;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: H or y in Ball Y,r )
reconsider Y9 = Y as Real ;
assume y in f .: H ; :: thesis: y in Ball Y,r
then consider x being set such that
A17: x in dom f and
A18: x in H and
A19: y = f . x by FUNCT_1:def 12;
reconsider x9 = x as Point of RealSpace by A18;
reconsider y9 = y as Real by A17, A19, FUNCT_2:7;
reconsider x99 = x9 as Real ;
reconsider yy = y9 as Point of RealSpace ;
A20: abs a > 0 by A14, COMPLEX1:133;
dist W9,x9 < r / (2 * (abs a)) by A18, METRIC_1:12;
then abs (W99 - x99) < r / (2 * (abs a)) by Th15;
then (abs a) * (abs (W99 - x99)) < (abs a) * (r / (2 * (abs a))) by A20, XREAL_1:70;
then abs (a * (W99 - x99)) < (abs a) * (r / (2 * (abs a))) by COMPLEX1:151;
then abs (((a * W99) + b) - ((a * x99) + b)) < (abs a) * (r / (2 * (abs a))) ;
then abs (Y9 - ((a * x99) + b)) < (abs a) * (r / (2 * (abs a))) by A1;
then A21: abs (Y9 - y9) < (abs a) * (r / (2 * (abs a))) by A1, A19;
abs a <> 0 by A14, ABSVALUE:7;
then A22: (abs a) * (r / (2 * (abs a))) = r / 2 by XCMPLX_1:93;
( (r / 2) + (r / 2) = r & r / 2 >= 0 ) by A6, XREAL_1:138;
then abs (Y9 - y9) < r by A21, A22, Lm2;
then dist Y,yy < r by Th15;
hence y in Ball Y,r by METRIC_1:12; :: thesis: verum

end;

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

end;

end;

end;

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

end;

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