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:22;
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:23;
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 6;
reconsider W9 = W as Real ;
A13: Int G c= G by TOPS_1:16;
f . W = (0 * W9) + b by A1, A8
.= b ;
then f .: H c= G by A2, A12, A13, ZFMISC_1:31;
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:23;
abs a > 0 by A14, COMPLEX1:47;
then 2 * (abs a) > 0 by XREAL_1:129;
then W in Int H by A6, A15, TBSP_1:11, XREAL_1:139;
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 6;
reconsider x9 = x as Point of RealSpace by A18;
reconsider y9 = y as Real by A17, A19, FUNCT_2:5;
reconsider x99 = x9 as Real ;
reconsider yy = y9 as Point of RealSpace ;
A20: abs a > 0 by A14, COMPLEX1:47;
dist (W9,x9) < r / (2 * (abs a)) by A18, METRIC_1:11;
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:68;
then abs (a * (W99 - x99)) < (abs a) * (r / (2 * (abs a))) by COMPLEX1:65;
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:2;
then A22: (abs a) * (r / (2 * (abs a))) = r / 2 by XCMPLX_1:92;
( (r / 2) + (r / 2) = r & r / 2 >= 0 ) by A6, XREAL_1:136;
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:11; :: 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 1; :: thesis: verum