now for y being object holds
( ( y in [.(- 1),1.] implies ex x being object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) ) & ( ex x being object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) implies y in [.(- 1),1.] ) )let y be
object ;
( ( y in [.(- 1),1.] implies ex x being object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) ) & ( ex x being object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) implies y in [.(- 1),1.] ) )thus
(
y in [.(- 1),1.] implies ex
x being
object st
(
x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) &
y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) )
( ex x being object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) implies y in [.(- 1),1.] )proof
A1:
(PI / 4) * 3
> PI / 4
by XREAL_1:155;
assume A2:
y in [.(- 1),1.]
;
ex x being object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x )
then reconsider y1 =
y as
Real ;
A3:
y1 in [.(cot . ((3 / 4) * PI)),(cot . (PI / 4)).] \/ [.(cot . (PI / 4)),(cot . ((3 / 4) * PI)).]
by A2, Th18, XBOOLE_0:def 3;
A4:
[.(PI / 4),((3 / 4) * PI).] c= ].0,PI.[
by Lm9, Lm10, XXREAL_2:def 12;
cot | ].0,PI.[ is
continuous
by Lm2, FDIFF_1:25;
then
cot | [.(PI / 4),((3 / 4) * PI).] is
continuous
by A4, FCONT_1:16;
then consider x being
Real such that A5:
x in [.(PI / 4),((3 / 4) * PI).]
and A6:
y1 = cot . x
by A1, A4, A3, Th2, FCONT_2:15, XBOOLE_1:1;
take
x
;
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x )
thus
(
x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) &
y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x )
by A5, A6, Lm12, FUNCT_1:49;
verum
end; thus
( ex
x being
object st
(
x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) &
y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) implies
y in [.(- 1),1.] )
verum end;
hence
rng (cot | [.(PI / 4),((3 / 4) * PI).]) = [.(- 1),1.]
by FUNCT_1:def 3; verum