now for y being object holds
( ( y in [.(PI / 4),((3 / 4) * PI).] implies ex x being object st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) ) & ( ex x being object st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) implies y in [.(PI / 4),((3 / 4) * PI).] ) )let y be
object ;
( ( y in [.(PI / 4),((3 / 4) * PI).] implies ex x being object st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) ) & ( ex x being object st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) implies y in [.(PI / 4),((3 / 4) * PI).] ) )thus
(
y in [.(PI / 4),((3 / 4) * PI).] implies ex
x being
object st
(
x in dom (arccot | [.(- 1),1.]) &
y = (arccot | [.(- 1),1.]) . x ) )
( ex x being object st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) implies y in [.(PI / 4),((3 / 4) * PI).] )proof
assume A1:
y in [.(PI / 4),((3 / 4) * PI).]
;
ex x being object st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x )
then reconsider y1 =
y as
Real ;
y1 in [.(arccot . 1),(arccot . (- 1)).] \/ [.(arccot . (- 1)),(arccot . 1).]
by A1, Th38, Th40, XBOOLE_0:def 3;
then consider x being
Real such that A2:
x in [.(- 1),1.]
and A3:
y1 = arccot . x
by Th24, Th54, FCONT_2:15;
take
x
;
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x )
thus
(
x in dom (arccot | [.(- 1),1.]) &
y = (arccot | [.(- 1),1.]) . x )
by A2, A3, Th24, FUNCT_1:49, RELAT_1:62;
verum
end; thus
( ex
x being
object st
(
x in dom (arccot | [.(- 1),1.]) &
y = (arccot | [.(- 1),1.]) . x ) implies
y in [.(PI / 4),((3 / 4) * PI).] )
verumproof
given x being
object such that A4:
x in dom (arccot | [.(- 1),1.])
and A5:
y = (arccot | [.(- 1),1.]) . x
;
y in [.(PI / 4),((3 / 4) * PI).]
A6:
dom (arccot | [.(- 1),1.]) = [.(- 1),1.]
by Th24, RELAT_1:62;
then
y = arccot . x
by A4, A5, FUNCT_1:49;
hence
y in [.(PI / 4),((3 / 4) * PI).]
by A4, A6, Th50;
verum
end; end;
hence
rng (arccot | [.(- 1),1.]) = [.(PI / 4),((3 / 4) * PI).]
by FUNCT_1:def 3; verum