:: FUNCT_8 semantic presentation
begin
definition
let
A
be ( ( ) ( )
set
) ;
attr
A
is
symmetrical
means
:: FUNCT_8:def 1
for
x
being ( (
complex
) (
complex
)
number
) st
x
: ( (
complex
) (
complex
)
number
)
in
A
: ( ( ) ( )
set
) holds
-
x
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
)
in
A
: ( ( ) ( )
set
) ;
end;
registration
cluster
complex-membered
symmetrical
for ( ( ) ( )
Element
of
K6
(
COMPLEX
: ( ( ) ( non
zero
V48
()
complex-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ;
end;
registration
cluster
complex-membered
ext-real-membered
real-membered
symmetrical
for ( ( ) ( )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ;
end;
definition
let
R
be ( (
Relation-like
) (
Relation-like
)
Relation
) ;
attr
R
is
with_symmetrical_domain
means
:: FUNCT_8:def 2
dom
R
: ( ( ) ( )
set
) : ( ( ) ( )
set
) is
symmetrical
;
end;
registration
cluster
empty
Relation-like
->
Relation-like
with_symmetrical_domain
for ( ( ) ( )
set
) ;
end;
registration
let
R
be ( (
Relation-like
with_symmetrical_domain
) (
Relation-like
with_symmetrical_domain
)
Relation
) ;
cluster
dom
R
: ( (
Relation-like
with_symmetrical_domain
) (
Relation-like
with_symmetrical_domain
)
set
) : ( ( ) ( )
set
)
->
symmetrical
;
end;
definition
let
X
,
Y
be ( (
complex-membered
) (
complex-membered
)
set
) ;
let
F
be ( (
Function-like
) (
Relation-like
X
: ( (
complex-membered
) (
complex-membered
)
set
)
-defined
Y
: ( (
complex-membered
) (
complex-membered
)
set
)
-valued
Function-like
V36
() )
PartFunc
of ,) ;
attr
F
is
quasi_even
means
:: FUNCT_8:def 3
for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
dom
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K6
(
X
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) &
-
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
in
dom
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K6
(
X
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) holds
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) )
.
(
-
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
)
=
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) )
.
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) ( )
set
) ;
end;
definition
let
X
,
Y
be ( (
complex-membered
) (
complex-membered
)
set
) ;
let
F
be ( (
Function-like
) (
Relation-like
X
: ( (
complex-membered
) (
complex-membered
)
set
)
-defined
Y
: ( (
complex-membered
) (
complex-membered
)
set
)
-valued
Function-like
V36
() )
PartFunc
of ,) ;
attr
F
is
even
means
:: FUNCT_8:def 4
(
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) is
with_symmetrical_domain
&
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) is
quasi_even
);
end;
registration
let
X
,
Y
be ( (
complex-membered
) (
complex-membered
)
set
) ;
cluster
Function-like
with_symmetrical_domain
quasi_even
->
Function-like
even
for ( ( ) ( )
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) ;
cluster
Function-like
even
->
Function-like
with_symmetrical_domain
quasi_even
for ( ( ) ( )
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) ;
end;
definition
let
A
be ( ( ) ( )
set
) ;
let
X
,
Y
be ( (
complex-membered
) (
complex-membered
)
set
) ;
let
F
be ( (
Function-like
) (
Relation-like
X
: ( (
complex-membered
) (
complex-membered
)
set
)
-defined
Y
: ( (
complex-membered
) (
complex-membered
)
set
)
-valued
Function-like
V36
() )
PartFunc
of ,) ;
pred
F
is_even_on
A
means
:: FUNCT_8:def 5
(
A
: ( ( ) ( )
set
)
c=
dom
F
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of
K6
(
X
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) &
F
: ( ( ) ( )
set
)
|
A
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) (
Relation-like
A
: ( ( ) ( )
set
)
-defined
X
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
A
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) )
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) (
Relation-like
A
: ( ( ) ( )
set
)
-defined
X
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
A
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) is
even
);
end;
definition
let
X
,
Y
be ( (
complex-membered
) (
complex-membered
)
set
) ;
let
F
be ( (
Function-like
) (
Relation-like
X
: ( (
complex-membered
) (
complex-membered
)
set
)
-defined
Y
: ( (
complex-membered
) (
complex-membered
)
set
)
-valued
Function-like
V36
() )
PartFunc
of ,) ;
attr
F
is
quasi_odd
means
:: FUNCT_8:def 6
for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
dom
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K6
(
X
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) &
-
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
in
dom
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K6
(
X
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) holds
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) )
.
(
-
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
)
=
-
(
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) )
.
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) ( )
set
) : ( (
complex
) (
complex
)
set
) ;
end;
definition
let
X
,
Y
be ( (
complex-membered
) (
complex-membered
)
set
) ;
let
F
be ( (
Function-like
) (
Relation-like
X
: ( (
complex-membered
) (
complex-membered
)
set
)
-defined
Y
: ( (
complex-membered
) (
complex-membered
)
set
)
-valued
Function-like
V36
() )
PartFunc
of ,) ;
attr
F
is
odd
means
:: FUNCT_8:def 7
(
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) is
with_symmetrical_domain
&
F
: ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) is
quasi_odd
);
end;
registration
let
X
,
Y
be ( (
complex-membered
) (
complex-membered
)
set
) ;
cluster
Function-like
with_symmetrical_domain
quasi_odd
->
Function-like
odd
for ( ( ) ( )
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) ;
cluster
Function-like
odd
->
Function-like
with_symmetrical_domain
quasi_odd
for ( ( ) ( )
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) ;
end;
definition
let
A
be ( ( ) ( )
set
) ;
let
X
,
Y
be ( (
complex-membered
) (
complex-membered
)
set
) ;
let
F
be ( (
Function-like
) (
Relation-like
X
: ( (
complex-membered
) (
complex-membered
)
set
)
-defined
Y
: ( (
complex-membered
) (
complex-membered
)
set
)
-valued
Function-like
V36
() )
PartFunc
of ,) ;
pred
F
is_odd_on
A
means
:: FUNCT_8:def 8
(
A
: ( ( ) ( )
set
)
c=
dom
F
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of
K6
(
X
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) &
F
: ( ( ) ( )
set
)
|
A
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
Y
: ( ( ) (
Relation-like
A
: ( ( ) ( )
set
)
-defined
X
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
A
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) )
-valued
)
Element
of
K6
(
K7
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) (
Relation-like
A
: ( ( ) ( )
set
)
-defined
X
: ( ( ) ( )
set
)
-valued
)
Element
of
K6
(
K7
(
A
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) is
odd
);
end;
theorem
:: FUNCT_8:1
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) holds
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) iff (
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) & ( for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
+
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
(
-
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
set
) : ( ( ) (
complex
real
ext-real
)
set
)
=
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ) ) ;
theorem
:: FUNCT_8:2
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) holds
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) iff (
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) & ( for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
-
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
(
-
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
set
) : ( ( ) (
complex
real
ext-real
)
set
)
=
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ) ) ;
theorem
:: FUNCT_8:3
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) & ( for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
set
)
<>
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ) holds
(
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) & ( for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
/
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
(
-
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
set
) : ( ( ) (
complex
real
ext-real
)
set
)
=
-
1 : ( ( ) ( non
zero
natural
complex
real
ext-real
positive
non
negative
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
zero
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ) ;
theorem
:: FUNCT_8:4
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) & ( for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
/
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
(
-
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
set
) : ( ( ) (
complex
real
ext-real
)
set
)
=
-
1 : ( ( ) ( non
zero
natural
complex
real
ext-real
positive
non
negative
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
zero
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:5
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) & ( for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
set
)
<>
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ) holds
(
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) & ( for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
/
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
(
-
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
set
) : ( ( ) (
complex
real
ext-real
)
set
)
=
1 : ( ( ) ( non
zero
natural
complex
real
ext-real
positive
non
negative
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ) ;
theorem
:: FUNCT_8:6
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) & ( for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
/
(
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
(
-
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
set
) : ( ( ) (
complex
real
ext-real
)
set
)
=
1 : ( ( ) ( non
zero
natural
complex
real
ext-real
positive
non
negative
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:7
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
set
)
=
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: FUNCT_8:8
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
set
)
=
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
(
abs
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
complex
real
ext-real
)
set
) ;
theorem
:: FUNCT_8:9
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) & ( for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
in
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
set
)
=
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.
(
abs
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
complex
real
ext-real
)
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:10
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
+
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:11
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
+
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:12
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
-
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:13
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
-
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:14
for
r
being ( ( ) (
complex
real
ext-real
)
Real
)
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
r
: ( ( ) (
complex
real
ext-real
)
Real
)
(#)
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:15
for
r
being ( ( ) (
complex
real
ext-real
)
Real
)
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
r
: ( ( ) (
complex
real
ext-real
)
Real
)
(#)
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:16
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
-
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:17
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
-
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:18
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
"
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:19
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
"
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:20
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
|.
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.|
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:21
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
|.
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.|
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:22
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
(#)
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:23
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
(#)
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:24
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
(#)
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:25
for
r
being ( ( ) (
complex
real
ext-real
)
Real
)
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
r
: ( ( ) (
complex
real
ext-real
)
Real
)
+
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:26
for
r
being ( ( ) (
complex
real
ext-real
)
Real
)
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
-
r
: ( ( ) (
complex
real
ext-real
)
Real
) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:27
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
^2
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:28
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
^2
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:29
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
/"
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:30
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
/"
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:31
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
/"
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:32
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_even_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) &
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
/"
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:33
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
holds
-
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
odd
;
theorem
:: FUNCT_8:34
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
holds
-
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:35
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
"
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
odd
;
theorem
:: FUNCT_8:36
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
"
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:37
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
holds
|.
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.|
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:38
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
holds
|.
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
.|
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:39
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
^2
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:40
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
^2
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:41
for
r
being ( ( ) (
complex
real
ext-real
)
Real
)
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
holds
r
: ( ( ) (
complex
real
ext-real
)
Real
)
+
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:42
for
r
being ( ( ) (
complex
real
ext-real
)
Real
)
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
-
r
: ( ( ) (
complex
real
ext-real
)
Real
) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:43
for
r
being ( ( ) (
complex
real
ext-real
)
Real
)
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
holds
r
: ( ( ) (
complex
real
ext-real
)
Real
)
(#)
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
odd
;
theorem
:: FUNCT_8:44
for
r
being ( ( ) (
complex
real
ext-real
)
Real
)
for
F
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
holds
r
: ( ( ) (
complex
real
ext-real
)
Real
)
(#)
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:45
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
+
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
odd
;
theorem
:: FUNCT_8:46
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
+
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:47
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
-
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
odd
;
theorem
:: FUNCT_8:48
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
-
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:49
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
(#)
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:50
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
(#)
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:51
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
(#)
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
odd
;
theorem
:: FUNCT_8:52
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
/"
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:53
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
/"
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
even
;
theorem
:: FUNCT_8:54
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
/"
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
odd
;
theorem
:: FUNCT_8:55
for
F
,
G
being ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) st
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
even
&
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) is
odd
&
(
dom
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) )
/\
(
dom
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) is
symmetrical
holds
F
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,)
/"
G
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
PartFunc
of ,) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) is
odd
;
begin
definition
func
signum
->
( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Function
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
means
:: FUNCT_8:def 9
for
x
being ( ( ) (
complex
real
ext-real
)
Real
) holds
it
: ( ( ) ( )
set
)
.
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
=
sgn
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ;
end;
theorem
:: FUNCT_8:56
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
>
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
signum
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Function
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
set
)
=
1 : ( ( ) ( non
zero
natural
complex
real
ext-real
positive
non
negative
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: FUNCT_8:57
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
<
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
signum
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Function
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
set
)
=
-
1 : ( ( ) ( non
zero
natural
complex
real
ext-real
positive
non
negative
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
zero
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ;
theorem
:: FUNCT_8:58
signum
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Function
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
.
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
=
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: FUNCT_8:59
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) holds
signum
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Function
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
.
(
-
x
: ( (
real
) (
complex
real
ext-real
)
number
)
)
: ( (
complex
) (
complex
real
ext-real
)
set
) : ( ( ) (
complex
real
ext-real
)
set
)
=
-
(
signum
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Function
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
set
) : ( (
complex
) (
complex
real
ext-real
)
set
) ;
theorem
:: FUNCT_8:60
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
signum
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Function
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:61
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
>=
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
absreal
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
set
)
=
x
: ( (
real
) (
complex
real
ext-real
)
number
) ;
theorem
:: FUNCT_8:62
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
<
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
absreal
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
set
)
=
-
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( (
complex
) (
complex
real
ext-real
)
set
) ;
theorem
:: FUNCT_8:63
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) holds
absreal
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
.
(
-
x
: ( (
real
) (
complex
real
ext-real
)
number
)
)
: ( (
complex
) (
complex
real
ext-real
)
set
) : ( ( ) (
complex
real
ext-real
)
set
)
=
absreal
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
set
) ;
theorem
:: FUNCT_8:64
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
absreal
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:65
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
sin
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:66
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
cos
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
registration
cluster
sin
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
->
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
odd
;
end;
registration
cluster
cos
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
->
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
even
;
end;
theorem
:: FUNCT_8:67
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
sinh
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:68
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
cosh
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
registration
cluster
sinh
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
->
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
odd
;
end;
registration
cluster
cosh
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
->
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
even
;
end;
theorem
:: FUNCT_8:69
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) st
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
].
(
-
(
PI
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
/
2 : ( ( ) ( non
zero
natural
complex
real
ext-real
positive
non
negative
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ,
(
PI
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
/
2 : ( ( ) ( non
zero
natural
complex
real
ext-real
positive
non
negative
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
.[
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) holds
tan
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:70
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) st
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
tan
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) holds
tan
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:71
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) st
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
cot
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) holds
cot
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:72
for
A
being ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) st
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
[.
(
-
1 : ( ( ) ( non
zero
natural
complex
real
ext-real
positive
non
negative
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
zero
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ,1 : ( ( ) ( non
zero
natural
complex
real
ext-real
positive
non
negative
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) )
.]
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) holds
arctan
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:73
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
|.
sin
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
()
with_symmetrical_domain
quasi_odd
odd
)
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
.|
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:74
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
|.
cos
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
()
with_symmetrical_domain
quasi_even
even
)
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
.|
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:75
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
sin
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
()
with_symmetrical_domain
quasi_odd
odd
)
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
"
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:76
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
cos
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
()
with_symmetrical_domain
quasi_even
even
)
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
"
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:77
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
-
sin
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
()
with_symmetrical_domain
quasi_odd
odd
)
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:78
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
-
cos
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
()
with_symmetrical_domain
quasi_even
even
)
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:79
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
sin
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
()
with_symmetrical_domain
quasi_odd
odd
)
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
^2
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:80
for
A
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
cos
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
()
with_symmetrical_domain
quasi_even
even
)
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
^2
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
A
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:81
for
B
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) st
B
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
sec
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) holds
sec
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
B
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:82
for
B
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) st ( for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
B
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
cos
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
()
with_symmetrical_domain
quasi_even
even
)
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
set
)
<>
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ) holds
sec
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_even_on
B
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:83
for
B
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) st
B
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) )
c=
dom
cosec
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) holds
cosec
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
B
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: FUNCT_8:84
for
B
being ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) st ( for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
B
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) holds
sin
: ( (
Function-like
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) ) ( non
zero
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
total
V33
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) )
V36
()
V37
()
V38
()
with_symmetrical_domain
quasi_odd
odd
)
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
set
)
<>
0
: ( ( ) (
zero
natural
complex
real
ext-real
non
positive
non
negative
Relation-like
non-empty
empty-yielding
RAT
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
rational-membered
V143
() )
set
)
-valued
Function-like
one-to-one
constant
functional
V36
()
V37
()
V38
()
V39
()
V46
()
V47
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
()
with_symmetrical_domain
)
Element
of
NAT
: ( ( ) (
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V143
() )
Element
of
K6
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) ( )
set
) ) ) ) holds
cosec
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-defined
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
)
-valued
Function-like
V36
()
V37
()
V38
() )
Element
of
K6
(
K7
(
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ,
REAL
: ( ( ) ( non
zero
V48
()
complex-membered
ext-real-membered
real-membered
V143
() )
set
) ) : ( ( ) (
Relation-like
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
is_odd_on
B
: ( (
symmetrical
) (
complex-membered
ext-real-membered
real-membered
symmetrical
)
Subset
of ( ( ) ( )
set
) ) ;