let f be Function of REAL,REAL; :: thesis: for a, b being Real st ( for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) holds

f is continuous

let a, b be Real; :: thesis: ( ( for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) implies f is continuous )

assume A3: for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ; :: thesis: f is continuous

reconsider f = f as PartFunc of REAL,REAL ;

for x0 being Real st x0 in dom f holds

f is_continuous_in x0

f is continuous

let a, b be Real; :: thesis: ( ( for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) implies f is continuous )

assume A3: for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ; :: thesis: f is continuous

reconsider f = f as PartFunc of REAL,REAL ;

for x0 being Real st x0 in dom f holds

f is_continuous_in x0

proof

hence
f is continuous
; :: thesis: verum
let x0 be Real; :: thesis: ( x0 in dom f implies f is_continuous_in x0 )

for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

end;for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

proof

hence
( x0 in dom f implies f is_continuous_in x0 )
by FCONT_1:4; :: thesis: verum
let N1 be Neighbourhood of f . x0; :: thesis: ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

consider g being Real such that

A1: 0 < g and

A2: N1 = ].((f . x0) - g),((f . x0) + g).[ by RCOMP_1:def 6;

ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1 ; :: thesis: verum

end;for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

consider g being Real such that

A1: 0 < g and

A2: N1 = ].((f . x0) - g),((f . x0) + g).[ by RCOMP_1:def 6;

ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

proof
end;

hence
ex N being Neighbourhood of x0 st per cases
( a = 0 or a <> 0 )
;

end;

suppose B1:
a = 0
; :: thesis: ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1 ; :: thesis: verum

end;for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

proof

hence
ex N being Neighbourhood of x0 st
take N = ].(x0 - g),(x0 + g).[; :: thesis: ( N is Neighbourhood of x0 & ( for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1 ) )

reconsider N = N as Neighbourhood of x0 by RCOMP_1:def 6, A1;

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

f . x1 in N1 ) ) ; :: thesis: verum

end;f . x1 in N1 ) )

reconsider N = N as Neighbourhood of x0 by RCOMP_1:def 6, A1;

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

proof

hence
( N is Neighbourhood of x0 & ( for x1 being Real st x1 in dom f & x1 in N holds
let x1 be Real; :: thesis: ( x1 in dom f & x1 in N implies f . x1 in N1 )

|.((f . x1) - (f . x0)).| = |.((f . x1) - (((1 / 2) * (sin ((a * x0) + b))) + (1 / 2))).| by A3

.= |.((((1 / 2) * (sin ((0 * x1) + b))) + (1 / 2)) - (((1 / 2) * (sin ((0 * x0) + b))) + (1 / 2))).| by B1, A3

.= 0 by ABSVALUE:def 1 ;

hence ( x1 in dom f & x1 in N implies f . x1 in N1 ) by A2, RCOMP_1:1, A1; :: thesis: verum

end;|.((f . x1) - (f . x0)).| = |.((f . x1) - (((1 / 2) * (sin ((a * x0) + b))) + (1 / 2))).| by A3

.= |.((((1 / 2) * (sin ((0 * x1) + b))) + (1 / 2)) - (((1 / 2) * (sin ((0 * x0) + b))) + (1 / 2))).| by B1, A3

.= 0 by ABSVALUE:def 1 ;

hence ( x1 in dom f & x1 in N implies f . x1 in N1 ) by A2, RCOMP_1:1, A1; :: thesis: verum

f . x1 in N1 ) ) ; :: thesis: verum

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1 ; :: thesis: verum

suppose B2:
a <> 0
; :: thesis: ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

AB:
( |.a.| > 0 & |.a.| <> 0 )
by COMPLEX1:47, B2;

ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1 ; :: thesis: verum

end;ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

proof

hence
ex N being Neighbourhood of x0 st
take N = ].(x0 - ((g * (1 / |.a.|)) * (1 / (1 / 2)))),(x0 + ((g * (1 / |.a.|)) * (1 / (1 / 2)))).[; :: thesis: ( N is Neighbourhood of x0 & ( for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1 ) )

reconsider N = N as Neighbourhood of x0 by RCOMP_1:def 6, A1, AB;

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

f . x1 in N1 ) ) ; :: thesis: verum

end;f . x1 in N1 ) )

reconsider N = N as Neighbourhood of x0 by RCOMP_1:def 6, A1, AB;

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

proof

hence
( N is Neighbourhood of x0 & ( for x1 being Real st x1 in dom f & x1 in N holds
let x1 be Real; :: thesis: ( x1 in dom f & x1 in N implies f . x1 in N1 )

assume x1 in dom f ; :: thesis: ( not x1 in N or f . x1 in N1 )

assume x1 in N ; :: thesis: f . x1 in N1

then |.(x1 - x0).| * ((1 / 2) * |.a.|) < ((g * (1 / |.a.|)) * (1 / (1 / 2))) * ((1 / 2) * |.a.|) by RCOMP_1:1, XREAL_1:68, AB;

then ((1 / 2) * |.a.|) * |.(x1 - x0).| < (((g * (1 / |.a.|)) * (1 / (1 / 2))) * (1 / 2)) * |.a.| ;

then ((1 / 2) * |.a.|) * |.(x1 - x0).| < (((g * |.(1 / a).|) * (1 / (1 / 2))) * (1 / 2)) * |.a.| by ABSVALUE:7;

then ((1 / 2) * |.a.|) * |.(x1 - x0).| < g * (|.(1 / a).| * |.a.|) ;

then E1a: ((1 / 2) * |.a.|) * |.(x1 - x0).| < g * 1 by ABSVALUE:6, B2;

E3: |.((f . x1) - (f . x0)).| = |.((f . x1) - (((1 / 2) * (sin ((a * x0) + b))) + (1 / 2))).| by A3

.= |.((((1 / 2) * (sin ((a * x1) + b))) + (1 / 2)) - (((1 / 2) * (sin ((a * x0) + b))) + (1 / 2))).| by A3

.= |.((1 / 2) * ((sin ((a * x1) + b)) - (sin ((a * x0) + b)))).|

.= |.(1 / 2).| * |.((sin ((a * x1) + b)) - (sin ((a * x0) + b))).| by COMPLEX1:65

.= (1 / 2) * |.((sin ((a * x1) + b)) - (sin ((a * x0) + b))).| by COMPLEX1:43 ;

(1 / 2) * |.(((a * x1) + b) - ((a * x0) + b)).| = (1 / 2) * |.(a * (x1 - x0)).|

.= (1 / 2) * (|.a.| * |.(x1 - x0).|) by COMPLEX1:65 ;

then |.((f . x1) - (f . x0)).| <= ((1 / 2) * |.a.|) * |.(x1 - x0).| by E3, LmSin2, XREAL_1:64;

then |.((f . x1) - (f . x0)).| < g by E1a, XXREAL_0:2;

hence f . x1 in N1 by A2, RCOMP_1:1; :: thesis: verum

end;assume x1 in dom f ; :: thesis: ( not x1 in N or f . x1 in N1 )

assume x1 in N ; :: thesis: f . x1 in N1

then |.(x1 - x0).| * ((1 / 2) * |.a.|) < ((g * (1 / |.a.|)) * (1 / (1 / 2))) * ((1 / 2) * |.a.|) by RCOMP_1:1, XREAL_1:68, AB;

then ((1 / 2) * |.a.|) * |.(x1 - x0).| < (((g * (1 / |.a.|)) * (1 / (1 / 2))) * (1 / 2)) * |.a.| ;

then ((1 / 2) * |.a.|) * |.(x1 - x0).| < (((g * |.(1 / a).|) * (1 / (1 / 2))) * (1 / 2)) * |.a.| by ABSVALUE:7;

then ((1 / 2) * |.a.|) * |.(x1 - x0).| < g * (|.(1 / a).| * |.a.|) ;

then E1a: ((1 / 2) * |.a.|) * |.(x1 - x0).| < g * 1 by ABSVALUE:6, B2;

E3: |.((f . x1) - (f . x0)).| = |.((f . x1) - (((1 / 2) * (sin ((a * x0) + b))) + (1 / 2))).| by A3

.= |.((((1 / 2) * (sin ((a * x1) + b))) + (1 / 2)) - (((1 / 2) * (sin ((a * x0) + b))) + (1 / 2))).| by A3

.= |.((1 / 2) * ((sin ((a * x1) + b)) - (sin ((a * x0) + b)))).|

.= |.(1 / 2).| * |.((sin ((a * x1) + b)) - (sin ((a * x0) + b))).| by COMPLEX1:65

.= (1 / 2) * |.((sin ((a * x1) + b)) - (sin ((a * x0) + b))).| by COMPLEX1:43 ;

(1 / 2) * |.(((a * x1) + b) - ((a * x0) + b)).| = (1 / 2) * |.(a * (x1 - x0)).|

.= (1 / 2) * (|.a.| * |.(x1 - x0).|) by COMPLEX1:65 ;

then |.((f . x1) - (f . x0)).| <= ((1 / 2) * |.a.|) * |.(x1 - x0).| by E3, LmSin2, XREAL_1:64;

then |.((f . x1) - (f . x0)).| < g by E1a, XXREAL_0:2;

hence f . x1 in N1 by A2, RCOMP_1:1; :: thesis: verum

f . x1 in N1 ) ) ; :: thesis: verum

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1 ; :: thesis: verum

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1 ; :: thesis: verum