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

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

hence
f is continuous
by BORSUK_1:def 1; :: thesis: verum
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;

end;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= Gend;

hence
ex H being a_neighborhood of W st f .: H c= G
; :: thesis: verumper cases
( a = 0 or a <> 0 )
;

end;

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 object holds

( y in {b} iff ex x being object st

( x in dom f & x in H & y = f . x ) )

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;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 object holds

( y in {b} iff ex x being object st

( x in dom f & x in H & y = f . x ) )

proof

then A12:
f .: H = {b}
by FUNCT_1:def 6;
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} )

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;( 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

given x being object such that A10:
x in dom f
and
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 = (0 * 0) + b by A1, A8

.= y by A9, TARSKI:def 1 ; :: thesis: verum

end;( 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 = (0 * 0) + b by A1, A8

.= y by A9, TARSKI:def 1 ; :: thesis: verum

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

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

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 A14, COMPLEX1:47;

then 2 * |.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)

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

end;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 A14, COMPLEX1:47;

then 2 * |.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

Ball (Y,r) c= G
by A4, A7;
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 A17, A19, FUNCT_2:5;

reconsider x99 = x9 as Real ;

reconsider yy = y9 as Point of RealSpace ;

A20: |.a.| > 0 by A14, COMPLEX1:47;

dist (W9,x9) < r / (2 * |.a.|) by A18, METRIC_1:11;

then |.(W99 - x99).| < r / (2 * |.a.|) by Th11;

then |.a.| * |.(W99 - x99).| < |.a.| * (r / (2 * |.a.|)) by A20, XREAL_1:68;

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 A1, A19;

|.a.| <> 0 by A14, ABSVALUE:2;

then A22: |.a.| * (r / (2 * |.a.|)) = r / 2 by XCMPLX_1:92;

( (r / 2) + (r / 2) = r & r / 2 >= 0 ) by A6, XREAL_1:136;

then |.(Y9 - y9).| < r by A21, A22, Lm2;

then dist (Y,yy) < r by Th11;

hence y in Ball (Y,r) by METRIC_1:11; :: thesis: verum

end;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 A17, A19, FUNCT_2:5;

reconsider x99 = x9 as Real ;

reconsider yy = y9 as Point of RealSpace ;

A20: |.a.| > 0 by A14, COMPLEX1:47;

dist (W9,x9) < r / (2 * |.a.|) by A18, METRIC_1:11;

then |.(W99 - x99).| < r / (2 * |.a.|) by Th11;

then |.a.| * |.(W99 - x99).| < |.a.| * (r / (2 * |.a.|)) by A20, XREAL_1:68;

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 A1, A19;

|.a.| <> 0 by A14, ABSVALUE:2;

then A22: |.a.| * (r / (2 * |.a.|)) = r / 2 by XCMPLX_1:92;

( (r / 2) + (r / 2) = r & r / 2 >= 0 ) by A6, XREAL_1:136;

then |.(Y9 - y9).| < r by A21, A22, Lm2;

then dist (Y,yy) < r by Th11;

hence y in Ball (Y,r) by METRIC_1:11; :: thesis: verum

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