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

proof

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

proof

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

proof

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

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

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

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

proof

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;

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

end;

hence ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds
f . x1 in N1 ; :: thesis: verum

end;

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

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

proof

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

proof

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;

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

end;

hence ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds
f . x1 in N1 ; :: thesis: verum

end;

end;

end;

hence ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds
f . x1 in N1 ; :: thesis: verum

end;

hence ( x0 in dom f implies f is_continuous_in x0 ) by FCONT_1:4; :: thesis: verum

end;

hence f is continuous ; :: thesis: verum