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 such that
A6: r > 0 and
A7: Ball (Y,r) c= Q by A3, A5, Th15;
now :: thesis: ex H being a_neighborhood of W st f .: H c= G
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 () by TOPS_1:23;
then reconsider H = [#] R^1 as a_neighborhood of W by CONNSP_2:def 1;
for y being object holds
( y in {b} iff ex x being object st
( x in dom f & x in H & y = f . x ) )
proof
let y be object ; :: thesis: ( y in {b} iff ex x being object st
( x in dom f & x in H & y = f . x ) )

thus ( y in {b} implies ex x being object st
( x in dom f & x in H & y = f . x ) ) :: thesis: ( ex x being object 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 object 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;
then ( In (0,REAL) in dom f & In (0,REAL) in H ) ;
hence ( 0 in dom f & 0 in H ) ; :: thesis: y = f . 0
thus f . 0 = () + b by A1, A8
.= y by ; :: thesis: verum
end;
given x being object 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 ;
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 * |.a.|);
reconsider H = Ball (W9,(r / (2 * |.a.|))) as Subset of R^1 ;
H is open by Th14;
then A15: Int H = H by TOPS_1:23;
|.a.| > 0 by ;
then 2 * |.a.| > 0 by XREAL_1:129;
then W in Int H by ;
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 object ; :: 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 object 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 Element of REAL by ;
reconsider x99 = x9 as Real ;
reconsider yy = y9 as Point of RealSpace ;
A20: |.a.| > 0 by ;
dist (W9,x9) < r / (2 * |.a.|) by ;
then |.(W99 - x99).| < r / (2 * |.a.|) by Th11;
then |.a.| * |.(W99 - x99).| < |.a.| * (r / (2 * |.a.|)) by ;
then |.(a * (W99 - x99)).| < |.a.| * (r / (2 * |.a.|)) by COMPLEX1:65;
then |.(((a * W99) + b) - ((a * x99) + b)).| < |.a.| * (r / (2 * |.a.|)) ;
then |.(Y9 - ((a * x99) + b)).| < |.a.| * (r / (2 * |.a.|)) by A1;
then A21: |.(Y9 - y9).| < |.a.| * (r / (2 * |.a.|)) by ;
|.a.| <> 0 by ;
then A22: |.a.| * (r / (2 * |.a.|)) = r / 2 by XCMPLX_1:92;
( (r / 2) + (r / 2) = r & r / 2 >= 0 ) by ;
then |.(Y9 - y9).| < r by ;
then dist (Y,yy) < r by Th11;
hence y in Ball (Y,r) by METRIC_1:11; :: thesis: verum
end;
Ball (Y,r) c= G by A4, A7;
hence ex H being a_neighborhood of W st f .: H c= G by ; :: 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