:: Number-Valued Functions
:: by Library Committee
::
:: Received November 22, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users
begin
definition
let
f
be
Relation
;
attr
f
is
complex-valued
means
:
Def1
:
:: VALUED_0:def 1
rng
f
c=
COMPLEX
;
attr
f
is
ext-real-valued
means
:
Def2
:
:: VALUED_0:def 2
rng
f
c=
ExtREAL
;
attr
f
is
real-valued
means
:
Def3
:
:: VALUED_0:def 3
rng
f
c=
REAL
;
canceled;
canceled;
attr
f
is
natural-valued
means
:
Def6
:
:: VALUED_0:def 6
rng
f
c=
NAT
;
end;
::
deftheorem
Def1
defines
complex-valued
VALUED_0:def 1 :
for
f
being
Relation
holds
(
f
is
complex-valued
iff
rng
f
c=
COMPLEX
);
::
deftheorem
Def2
defines
ext-real-valued
VALUED_0:def 2 :
for
f
being
Relation
holds
(
f
is
ext-real-valued
iff
rng
f
c=
ExtREAL
);
::
deftheorem
Def3
defines
real-valued
VALUED_0:def 3 :
for
f
being
Relation
holds
(
f
is
real-valued
iff
rng
f
c=
REAL
);
::
deftheorem
VALUED_0:def 4 :
canceled;
::
deftheorem
VALUED_0:def 5 :
canceled;
::
deftheorem
Def6
defines
natural-valued
VALUED_0:def 6 :
for
f
being
Relation
holds
(
f
is
natural-valued
iff
rng
f
c=
NAT
);
registration
cluster
Relation-like
natural-valued
->
INT
-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
natural-valued
holds
b
1
is
INT
-valued
proof
end;
cluster
Relation-like
INT
-valued
->
RAT
-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
INT
-valued
holds
b
1
is
RAT
-valued
proof
end;
cluster
Relation-like
INT
-valued
->
real-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
INT
-valued
holds
b
1
is
real-valued
proof
end;
cluster
Relation-like
RAT
-valued
->
real-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
RAT
-valued
holds
b
1
is
real-valued
proof
end;
cluster
Relation-like
real-valued
->
ext-real-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
real-valued
holds
b
1
is
ext-real-valued
proof
end;
cluster
Relation-like
real-valued
->
complex-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
real-valued
holds
b
1
is
complex-valued
proof
end;
cluster
Relation-like
natural-valued
->
RAT
-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
natural-valued
holds
b
1
is
RAT
-valued
proof
end;
cluster
Relation-like
natural-valued
->
real-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
natural-valued
holds
b
1
is
real-valued
proof
end;
end;
registration
cluster
empty
Relation-like
->
natural-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
empty
holds
b
1
is
natural-valued
proof
end;
end;
registration
cluster
Relation-like
Function-like
natural-valued
for
set
;
existence
ex
b
1
being
Function
st
b
1
is
natural-valued
proof
end;
end;
registration
let
R
be
complex-valued
Relation
;
cluster
rng
R
->
complex-membered
;
coherence
rng
R
is
complex-membered
proof
end;
end;
registration
let
R
be
ext-real-valued
Relation
;
cluster
rng
R
->
ext-real-membered
;
coherence
rng
R
is
ext-real-membered
proof
end;
end;
registration
let
R
be
real-valued
Relation
;
cluster
rng
R
->
real-membered
;
coherence
rng
R
is
real-membered
proof
end;
end;
registration
let
R
be
RAT
-valued
Relation
;
cluster
rng
R
->
rational-membered
;
coherence
rng
R
is
rational-membered
;
end;
registration
let
R
be
INT
-valued
Relation
;
cluster
rng
R
->
integer-membered
;
coherence
rng
R
is
integer-membered
;
end;
registration
let
R
be
natural-valued
Relation
;
cluster
rng
R
->
natural-membered
;
coherence
rng
R
is
natural-membered
proof
end;
end;
theorem
Th1
:
:: VALUED_0:1
for
R
being
Relation
for
S
being
complex-valued
Relation
st
R
c=
S
holds
R
is
complex-valued
proof
end;
theorem
Th2
:
:: VALUED_0:2
for
R
being
Relation
for
S
being
ext-real-valued
Relation
st
R
c=
S
holds
R
is
ext-real-valued
proof
end;
theorem
Th3
:
:: VALUED_0:3
for
R
being
Relation
for
S
being
real-valued
Relation
st
R
c=
S
holds
R
is
real-valued
proof
end;
theorem
:: VALUED_0:4
for
R
being
Relation
for
S
being
RAT
-valued
Relation
st
R
c=
S
holds
R
is
RAT
-valued
;
theorem
:: VALUED_0:5
for
R
being
Relation
for
S
being
INT
-valued
Relation
st
R
c=
S
holds
R
is
INT
-valued
;
theorem
Th6
:
:: VALUED_0:6
for
R
being
Relation
for
S
being
natural-valued
Relation
st
R
c=
S
holds
R
is
natural-valued
proof
end;
registration
let
R
be
complex-valued
Relation
;
cluster
->
complex-valued
for
Element
of
bool
R
;
coherence
for
b
1
being
Subset
of
R
holds
b
1
is
complex-valued
by
Th1
;
end;
registration
let
R
be
ext-real-valued
Relation
;
cluster
->
ext-real-valued
for
Element
of
bool
R
;
coherence
for
b
1
being
Subset
of
R
holds
b
1
is
ext-real-valued
by
Th2
;
end;
registration
let
R
be
real-valued
Relation
;
cluster
->
real-valued
for
Element
of
bool
R
;
coherence
for
b
1
being
Subset
of
R
holds
b
1
is
real-valued
by
Th3
;
end;
registration
let
R
be
RAT
-valued
Relation
;
cluster
->
RAT
-valued
for
Element
of
bool
R
;
coherence
for
b
1
being
Subset
of
R
holds
b
1
is
RAT
-valued
;
end;
registration
let
R
be
INT
-valued
Relation
;
cluster
->
INT
-valued
for
Element
of
bool
R
;
coherence
for
b
1
being
Subset
of
R
holds
b
1
is
INT
-valued
;
end;
registration
let
R
be
natural-valued
Relation
;
cluster
->
natural-valued
for
Element
of
bool
R
;
coherence
for
b
1
being
Subset
of
R
holds
b
1
is
natural-valued
by
Th6
;
end;
registration
let
R
,
S
be
complex-valued
Relation
;
cluster
R
\/
S
->
complex-valued
;
coherence
R
\/
S
is
complex-valued
proof
end;
end;
registration
let
R
,
S
be
ext-real-valued
Relation
;
cluster
R
\/
S
->
ext-real-valued
;
coherence
R
\/
S
is
ext-real-valued
proof
end;
end;
registration
let
R
,
S
be
real-valued
Relation
;
cluster
R
\/
S
->
real-valued
;
coherence
R
\/
S
is
real-valued
proof
end;
end;
registration
let
R
,
S
be
RAT
-valued
Relation
;
cluster
R
\/
S
->
RAT
-valued
;
coherence
R
\/
S
is
RAT
-valued
;
end;
registration
let
R
,
S
be
INT
-valued
Relation
;
cluster
R
\/
S
->
INT
-valued
;
coherence
R
\/
S
is
INT
-valued
;
end;
registration
let
R
,
S
be
natural-valued
Relation
;
cluster
R
\/
S
->
natural-valued
;
coherence
R
\/
S
is
natural-valued
proof
end;
end;
registration
let
R
be
complex-valued
Relation
;
let
S
be
Relation
;
cluster
R
/\
S
->
complex-valued
;
coherence
R
/\
S
is
complex-valued
proof
end;
cluster
R
\
S
->
complex-valued
;
coherence
R
\
S
is
complex-valued
;
end;
registration
let
R
be
ext-real-valued
Relation
;
let
S
be
Relation
;
cluster
R
/\
S
->
ext-real-valued
;
coherence
R
/\
S
is
ext-real-valued
proof
end;
cluster
R
\
S
->
ext-real-valued
;
coherence
R
\
S
is
ext-real-valued
;
end;
registration
let
R
be
real-valued
Relation
;
let
S
be
Relation
;
cluster
R
/\
S
->
real-valued
;
coherence
R
/\
S
is
real-valued
proof
end;
cluster
R
\
S
->
real-valued
;
coherence
R
\
S
is
real-valued
;
end;
registration
let
R
be
RAT
-valued
Relation
;
let
S
be
Relation
;
cluster
R
/\
S
->
RAT
-valued
;
coherence
R
/\
S
is
RAT
-valued
;
cluster
R
\
S
->
RAT
-valued
;
coherence
R
\
S
is
RAT
-valued
;
end;
registration
let
R
be
INT
-valued
Relation
;
let
S
be
Relation
;
cluster
R
/\
S
->
INT
-valued
;
coherence
R
/\
S
is
INT
-valued
;
cluster
R
\
S
->
INT
-valued
;
coherence
R
\
S
is
INT
-valued
;
end;
registration
let
R
be
natural-valued
Relation
;
let
S
be
Relation
;
cluster
R
/\
S
->
natural-valued
;
coherence
R
/\
S
is
natural-valued
proof
end;
cluster
R
\
S
->
natural-valued
;
coherence
R
\
S
is
natural-valued
;
end;
registration
let
R
,
S
be
complex-valued
Relation
;
cluster
R
\+\
S
->
complex-valued
;
coherence
R
\+\
S
is
complex-valued
;
end;
registration
let
R
,
S
be
ext-real-valued
Relation
;
cluster
R
\+\
S
->
ext-real-valued
;
coherence
R
\+\
S
is
ext-real-valued
;
end;
registration
let
R
,
S
be
real-valued
Relation
;
cluster
R
\+\
S
->
real-valued
;
coherence
R
\+\
S
is
real-valued
;
end;
registration
let
R
,
S
be
RAT
-valued
Relation
;
cluster
R
\+\
S
->
RAT
-valued
;
coherence
R
\+\
S
is
RAT
-valued
;
end;
registration
let
R
,
S
be
INT
-valued
Relation
;
cluster
R
\+\
S
->
INT
-valued
;
coherence
R
\+\
S
is
INT
-valued
;
end;
registration
let
R
,
S
be
natural-valued
Relation
;
cluster
R
\+\
S
->
natural-valued
;
coherence
R
\+\
S
is
natural-valued
;
end;
registration
let
R
be
complex-valued
Relation
;
let
X
be
set
;
cluster
R
.:
X
->
complex-membered
;
coherence
R
.:
X
is
complex-membered
proof
end;
end;
registration
let
R
be
ext-real-valued
Relation
;
let
X
be
set
;
cluster
R
.:
X
->
ext-real-membered
;
coherence
R
.:
X
is
ext-real-membered
proof
end;
end;
registration
let
R
be
real-valued
Relation
;
let
X
be
set
;
cluster
R
.:
X
->
real-membered
;
coherence
R
.:
X
is
real-membered
proof
end;
end;
registration
let
R
be
RAT
-valued
Relation
;
let
X
be
set
;
cluster
R
.:
X
->
rational-membered
;
coherence
R
.:
X
is
rational-membered
proof
end;
end;
registration
let
R
be
INT
-valued
Relation
;
let
X
be
set
;
cluster
R
.:
X
->
integer-membered
;
coherence
R
.:
X
is
integer-membered
proof
end;
end;
registration
let
R
be
natural-valued
Relation
;
let
X
be
set
;
cluster
R
.:
X
->
natural-membered
;
coherence
R
.:
X
is
natural-membered
proof
end;
end;
registration
let
R
be
complex-valued
Relation
;
let
x
be
set
;
cluster
Im
(
R
,
x
)
->
complex-membered
;
coherence
Im
(
R
,
x
) is
complex-membered
;
end;
registration
let
R
be
ext-real-valued
Relation
;
let
x
be
set
;
cluster
Im
(
R
,
x
)
->
ext-real-membered
;
coherence
Im
(
R
,
x
) is
ext-real-membered
;
end;
registration
let
R
be
real-valued
Relation
;
let
x
be
set
;
cluster
Im
(
R
,
x
)
->
real-membered
;
coherence
Im
(
R
,
x
) is
real-membered
;
end;
registration
let
R
be
RAT
-valued
Relation
;
let
x
be
set
;
cluster
Im
(
R
,
x
)
->
rational-membered
;
coherence
Im
(
R
,
x
) is
rational-membered
;
end;
registration
let
R
be
INT
-valued
Relation
;
let
x
be
set
;
cluster
Im
(
R
,
x
)
->
integer-membered
;
coherence
Im
(
R
,
x
) is
integer-membered
;
end;
registration
let
R
be
natural-valued
Relation
;
let
x
be
set
;
cluster
Im
(
R
,
x
)
->
natural-membered
;
coherence
Im
(
R
,
x
) is
natural-membered
;
end;
registration
let
R
be
complex-valued
Relation
;
let
X
be
set
;
cluster
R
|
X
->
complex-valued
;
coherence
R
|
X
is
complex-valued
proof
end;
end;
registration
let
R
be
ext-real-valued
Relation
;
let
X
be
set
;
cluster
R
|
X
->
ext-real-valued
;
coherence
R
|
X
is
ext-real-valued
proof
end;
end;
registration
let
R
be
real-valued
Relation
;
let
X
be
set
;
cluster
R
|
X
->
real-valued
;
coherence
R
|
X
is
real-valued
proof
end;
end;
registration
let
R
be
RAT
-valued
Relation
;
let
X
be
set
;
cluster
R
|
X
->
RAT
-valued
;
coherence
R
|
X
is
RAT
-valued
;
end;
registration
let
R
be
INT
-valued
Relation
;
let
X
be
set
;
cluster
R
|
X
->
INT
-valued
;
coherence
R
|
X
is
INT
-valued
;
end;
registration
let
R
be
natural-valued
Relation
;
let
X
be
set
;
cluster
R
|
X
->
natural-valued
;
coherence
R
|
X
is
natural-valued
proof
end;
end;
registration
let
X
be
complex-membered
set
;
cluster
id
X
->
complex-valued
;
coherence
id
X
is
complex-valued
proof
end;
end;
registration
let
X
be
ext-real-membered
set
;
cluster
id
X
->
ext-real-valued
;
coherence
id
X
is
ext-real-valued
proof
end;
end;
registration
let
X
be
real-membered
set
;
cluster
id
X
->
real-valued
;
coherence
id
X
is
real-valued
proof
end;
end;
registration
let
X
be
rational-membered
set
;
cluster
id
X
->
RAT
-valued
;
coherence
id
X
is
RAT
-valued
proof
end;
end;
registration
let
X
be
integer-membered
set
;
cluster
id
X
->
INT
-valued
;
coherence
id
X
is
INT
-valued
proof
end;
end;
registration
let
X
be
natural-membered
set
;
cluster
id
X
->
natural-valued
;
coherence
id
X
is
natural-valued
proof
end;
end;
registration
let
R
be
Relation
;
let
S
be
complex-valued
Relation
;
cluster
R
*
S
->
complex-valued
;
coherence
R
*
S
is
complex-valued
proof
end;
end;
registration
let
R
be
Relation
;
let
S
be
ext-real-valued
Relation
;
cluster
R
*
S
->
ext-real-valued
;
coherence
R
*
S
is
ext-real-valued
proof
end;
end;
registration
let
R
be
Relation
;
let
S
be
real-valued
Relation
;
cluster
R
*
S
->
real-valued
;
coherence
R
*
S
is
real-valued
proof
end;
end;
registration
let
R
be
Relation
;
let
S
be
RAT
-valued
Relation
;
cluster
R
*
S
->
RAT
-valued
;
coherence
R
*
S
is
RAT
-valued
;
end;
registration
let
R
be
Relation
;
let
S
be
INT
-valued
Relation
;
cluster
R
*
S
->
INT
-valued
;
coherence
R
*
S
is
INT
-valued
;
end;
registration
let
R
be
Relation
;
let
S
be
natural-valued
Relation
;
cluster
R
*
S
->
natural-valued
;
coherence
R
*
S
is
natural-valued
proof
end;
end;
definition
let
f
be
Function
;
redefine
attr
f
is
complex-valued
means
:
Def7
:
:: VALUED_0:def 7
for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
complex
;
compatibility
(
f
is
complex-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
complex
)
proof
end;
redefine
attr
f
is
ext-real-valued
means
:
Def8
:
:: VALUED_0:def 8
for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
ext-real
;
compatibility
(
f
is
ext-real-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
ext-real
)
proof
end;
redefine
attr
f
is
real-valued
means
:
Def9
:
:: VALUED_0:def 9
for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
real
;
compatibility
(
f
is
real-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
real
)
proof
end;
canceled;
canceled;
redefine
attr
f
is
natural-valued
means
:
Def12
:
:: VALUED_0:def 12
for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
natural
;
compatibility
(
f
is
natural-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
natural
)
proof
end;
end;
::
deftheorem
Def7
defines
complex-valued
VALUED_0:def 7 :
for
f
being
Function
holds
(
f
is
complex-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
complex
);
::
deftheorem
Def8
defines
ext-real-valued
VALUED_0:def 8 :
for
f
being
Function
holds
(
f
is
ext-real-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
ext-real
);
::
deftheorem
Def9
defines
real-valued
VALUED_0:def 9 :
for
f
being
Function
holds
(
f
is
real-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
real
);
::
deftheorem
VALUED_0:def 10 :
canceled;
::
deftheorem
VALUED_0:def 11 :
canceled;
::
deftheorem
Def12
defines
natural-valued
VALUED_0:def 12 :
for
f
being
Function
holds
(
f
is
natural-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
natural
);
theorem
Th7
:
:: VALUED_0:7
for
f
being
Function
holds
(
f
is
complex-valued
iff for
x
being
set
holds
f
.
x
is
complex
)
proof
end;
theorem
Th8
:
:: VALUED_0:8
for
f
being
Function
holds
(
f
is
ext-real-valued
iff for
x
being
set
holds
f
.
x
is
ext-real
)
proof
end;
theorem
Th9
:
:: VALUED_0:9
for
f
being
Function
holds
(
f
is
real-valued
iff for
x
being
set
holds
f
.
x
is
real
)
proof
end;
theorem
Th10
:
:: VALUED_0:10
for
f
being
Function
holds
(
f
is
RAT
-valued
iff for
x
being
set
holds
f
.
x
is
rational
)
proof
end;
theorem
Th11
:
:: VALUED_0:11
for
f
being
Function
holds
(
f
is
INT
-valued
iff for
x
being
set
holds
f
.
x
is
integer
)
proof
end;
theorem
Th12
:
:: VALUED_0:12
for
f
being
Function
holds
(
f
is
natural-valued
iff for
x
being
set
holds
f
.
x
is
natural
)
proof
end;
registration
let
f
be
complex-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
complex
;
coherence
f
.
x
is
complex
by
Th7
;
end;
registration
let
f
be
ext-real-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
ext-real
;
coherence
f
.
x
is
ext-real
by
Th8
;
end;
registration
let
f
be
real-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
real
;
coherence
f
.
x
is
real
by
Th9
;
end;
registration
let
f
be
RAT
-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
rational
;
coherence
f
.
x
is
rational
by
Th10
;
end;
registration
let
f
be
INT
-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
integer
;
coherence
f
.
x
is
integer
by
Th11
;
end;
registration
let
f
be
natural-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
natural
;
coherence
f
.
x
is
natural
by
Th12
;
end;
registration
let
X
be
set
;
let
x
be
complex
number
;
cluster
X
-->
x
->
complex-valued
;
coherence
X
-->
x
is
complex-valued
proof
end;
end;
registration
let
X
be
set
;
let
x
be
ext-real
number
;
cluster
X
-->
x
->
ext-real-valued
;
coherence
X
-->
x
is
ext-real-valued
proof
end;
end;
registration
let
X
be
set
;
let
x
be
real
number
;
cluster
X
-->
x
->
real-valued
;
coherence
X
-->
x
is
real-valued
proof
end;
end;
registration
let
X
be
set
;
let
x
be
rational
number
;
cluster
X
-->
x
->
RAT
-valued
;
coherence
X
-->
x
is
RAT
-valued
proof
end;
end;
registration
let
X
be
set
;
let
x
be
integer
number
;
cluster
X
-->
x
->
INT
-valued
;
coherence
X
-->
x
is
INT
-valued
proof
end;
end;
registration
let
X
be
set
;
let
x
be
Nat
;
cluster
X
-->
x
->
natural-valued
;
coherence
X
-->
x
is
natural-valued
proof
end;
end;
registration
let
f
,
g
be
complex-valued
Function
;
cluster
f
+*
g
->
complex-valued
;
coherence
f
+*
g
is
complex-valued
proof
end;
end;
registration
let
f
,
g
be
ext-real-valued
Function
;
cluster
f
+*
g
->
ext-real-valued
;
coherence
f
+*
g
is
ext-real-valued
proof
end;
end;
registration
let
f
,
g
be
real-valued
Function
;
cluster
f
+*
g
->
real-valued
;
coherence
f
+*
g
is
real-valued
proof
end;
end;
registration
let
f
,
g
be
RAT
-valued
Function
;
cluster
f
+*
g
->
RAT
-valued
;
coherence
f
+*
g
is
RAT
-valued
proof
end;
end;
registration
let
f
,
g
be
INT
-valued
Function
;
cluster
f
+*
g
->
INT
-valued
;
coherence
f
+*
g
is
INT
-valued
proof
end;
end;
registration
let
f
,
g
be
natural-valued
Function
;
cluster
f
+*
g
->
natural-valued
;
coherence
f
+*
g
is
natural-valued
proof
end;
end;
registration
let
x
be
set
;
let
y
be
complex
number
;
cluster
x
.-->
y
->
complex-valued
;
coherence
x
.-->
y
is
complex-valued
;
end;
registration
let
x
be
set
;
let
y
be
ext-real
number
;
cluster
x
.-->
y
->
ext-real-valued
;
coherence
x
.-->
y
is
ext-real-valued
;
end;
registration
let
x
be
set
;
let
y
be
real
number
;
cluster
x
.-->
y
->
real-valued
;
coherence
x
.-->
y
is
real-valued
;
end;
registration
let
x
be
set
;
let
y
be
rational
number
;
cluster
x
.-->
y
->
RAT
-valued
;
coherence
x
.-->
y
is
RAT
-valued
;
end;
registration
let
x
be
set
;
let
y
be
integer
number
;
cluster
x
.-->
y
->
INT
-valued
;
coherence
x
.-->
y
is
INT
-valued
;
end;
registration
let
x
be
set
;
let
y
be
Nat
;
cluster
x
.-->
y
->
natural-valued
;
coherence
x
.-->
y
is
natural-valued
;
end;
registration
let
X
be
set
;
let
Y
be
complex-membered
set
;
cluster
->
complex-valued
for
Element
of
bool
[:
X
,
Y
:]
;
coherence
for
b
1
being
Relation
of
X
,
Y
holds
b
1
is
complex-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
ext-real-membered
set
;
cluster
->
ext-real-valued
for
Element
of
bool
[:
X
,
Y
:]
;
coherence
for
b
1
being
Relation
of
X
,
Y
holds
b
1
is
ext-real-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
real-membered
set
;
cluster
->
real-valued
for
Element
of
bool
[:
X
,
Y
:]
;
coherence
for
b
1
being
Relation
of
X
,
Y
holds
b
1
is
real-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
rational-membered
set
;
cluster
->
RAT
-valued
for
Element
of
bool
[:
X
,
Y
:]
;
coherence
for
b
1
being
Relation
of
X
,
Y
holds
b
1
is
RAT
-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
integer-membered
set
;
cluster
->
INT
-valued
for
Element
of
bool
[:
X
,
Y
:]
;
coherence
for
b
1
being
Relation
of
X
,
Y
holds
b
1
is
INT
-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
natural-membered
set
;
cluster
->
natural-valued
for
Element
of
bool
[:
X
,
Y
:]
;
coherence
for
b
1
being
Relation
of
X
,
Y
holds
b
1
is
natural-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
complex-membered
set
;
cluster
[:
X
,
Y
:]
->
complex-valued
;
coherence
[:
X
,
Y
:]
is
complex-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
ext-real-membered
set
;
cluster
[:
X
,
Y
:]
->
ext-real-valued
;
coherence
[:
X
,
Y
:]
is
ext-real-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
real-membered
set
;
cluster
[:
X
,
Y
:]
->
real-valued
;
coherence
[:
X
,
Y
:]
is
real-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
rational-membered
set
;
cluster
[:
X
,
Y
:]
->
RAT
-valued
;
coherence
[:
X
,
Y
:]
is
RAT
-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
integer-membered
set
;
cluster
[:
X
,
Y
:]
->
INT
-valued
;
coherence
[:
X
,
Y
:]
is
INT
-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
natural-membered
set
;
cluster
[:
X
,
Y
:]
->
natural-valued
;
coherence
[:
X
,
Y
:]
is
natural-valued
proof
end;
end;
notation
let
f
be
ext-real-valued
Relation
;
synonym
non-zero
f
for
non-empty
;
end;
registration
cluster
non
empty
Relation-like
RAT
-valued
INT
-valued
Function-like
constant
natural-valued
for
set
;
existence
ex
b
1
being
Function
st
( not
b
1
is
empty
&
b
1
is
constant
&
b
1
is
natural-valued
&
b
1
is
INT
-valued
&
b
1
is
RAT
-valued
)
proof
end;
end;
theorem
:: VALUED_0:13
for
f
being non
empty
constant
complex-valued
Function
ex
r
being
complex
number
st
for
x
being
set
st
x
in
dom
f
holds
f
.
x
=
r
proof
end;
theorem
:: VALUED_0:14
for
f
being non
empty
constant
ext-real-valued
Function
ex
r
being
ext-real
number
st
for
x
being
set
st
x
in
dom
f
holds
f
.
x
=
r
proof
end;
theorem
:: VALUED_0:15
for
f
being non
empty
constant
real-valued
Function
ex
r
being
real
number
st
for
x
being
set
st
x
in
dom
f
holds
f
.
x
=
r
proof
end;
theorem
:: VALUED_0:16
for
f
being non
empty
RAT
-valued
constant
Function
ex
r
being
rational
number
st
for
x
being
set
st
x
in
dom
f
holds
f
.
x
=
r
proof
end;
theorem
:: VALUED_0:17
for
f
being non
empty
INT
-valued
constant
Function
ex
r
being
integer
number
st
for
x
being
set
st
x
in
dom
f
holds
f
.
x
=
r
proof
end;
theorem
:: VALUED_0:18
for
f
being non
empty
constant
natural-valued
Function
ex
r
being
Nat
st
for
x
being
set
st
x
in
dom
f
holds
f
.
x
=
r
proof
end;
begin
definition
let
f
be
ext-real-valued
Function
;
attr
f
is
increasing
means
:
Def13
:
:: VALUED_0:def 13
for
e1
,
e2
being
ext-real
number
st
e1
in
dom
f
&
e2
in
dom
f
&
e1
<
e2
holds
f
.
e1
<
f
.
e2
;
attr
f
is
decreasing
means
:
Def14
:
:: VALUED_0:def 14
for
e1
,
e2
being
ext-real
number
st
e1
in
dom
f
&
e2
in
dom
f
&
e1
<
e2
holds
f
.
e1
>
f
.
e2
;
attr
f
is
non-decreasing
means
:
Def15
:
:: VALUED_0:def 15
for
e1
,
e2
being
ext-real
number
st
e1
in
dom
f
&
e2
in
dom
f
&
e1
<=
e2
holds
f
.
e1
<=
f
.
e2
;
attr
f
is
non-increasing
means
:
Def16
:
:: VALUED_0:def 16
for
e1
,
e2
being
ext-real
number
st
e1
in
dom
f
&
e2
in
dom
f
&
e1
<=
e2
holds
f
.
e1
>=
f
.
e2
;
end;
::
deftheorem
Def13
defines
increasing
VALUED_0:def 13 :
for
f
being
ext-real-valued
Function
holds
(
f
is
increasing
iff for
e1
,
e2
being
ext-real
number
st
e1
in
dom
f
&
e2
in
dom
f
&
e1
<
e2
holds
f
.
e1
<
f
.
e2
);
::
deftheorem
Def14
defines
decreasing
VALUED_0:def 14 :
for
f
being
ext-real-valued
Function
holds
(
f
is
decreasing
iff for
e1
,
e2
being
ext-real
number
st
e1
in
dom
f
&
e2
in
dom
f
&
e1
<
e2
holds
f
.
e1
>
f
.
e2
);
::
deftheorem
Def15
defines
non-decreasing
VALUED_0:def 15 :
for
f
being
ext-real-valued
Function
holds
(
f
is
non-decreasing
iff for
e1
,
e2
being
ext-real
number
st
e1
in
dom
f
&
e2
in
dom
f
&
e1
<=
e2
holds
f
.
e1
<=
f
.
e2
);
::
deftheorem
Def16
defines
non-increasing
VALUED_0:def 16 :
for
f
being
ext-real-valued
Function
holds
(
f
is
non-increasing
iff for
e1
,
e2
being
ext-real
number
st
e1
in
dom
f
&
e2
in
dom
f
&
e1
<=
e2
holds
f
.
e1
>=
f
.
e2
);
:: 2008.08.31, A.T.
registration
cluster
trivial
Relation-like
Function-like
ext-real-valued
->
ext-real-valued
increasing
decreasing
for
set
;
coherence
for
b
1
being
ext-real-valued
Function
st
b
1
is
trivial
holds
(
b
1
is
increasing
&
b
1
is
decreasing
)
proof
end;
end;
registration
cluster
Relation-like
Function-like
ext-real-valued
increasing
->
ext-real-valued
non-decreasing
for
set
;
coherence
for
b
1
being
ext-real-valued
Function
st
b
1
is
increasing
holds
b
1
is
non-decreasing
proof
end;
cluster
Relation-like
Function-like
ext-real-valued
decreasing
->
ext-real-valued
non-increasing
for
set
;
coherence
for
b
1
being
ext-real-valued
Function
st
b
1
is
decreasing
holds
b
1
is
non-increasing
proof
end;
end;
registration
let
f
,
g
be
ext-real-valued
increasing
Function
;
cluster
f
*
g
->
increasing
;
coherence
g
*
f
is
increasing
proof
end;
end;
registration
let
f
,
g
be
ext-real-valued
non-decreasing
Function
;
cluster
f
*
g
->
non-decreasing
;
coherence
g
*
f
is
non-decreasing
proof
end;
end;
registration
let
f
,
g
be
ext-real-valued
decreasing
Function
;
cluster
f
*
g
->
increasing
;
coherence
g
*
f
is
increasing
proof
end;
end;
registration
let
f
,
g
be
ext-real-valued
non-increasing
Function
;
cluster
f
*
g
->
non-decreasing
;
coherence
g
*
f
is
non-decreasing
proof
end;
end;
registration
let
f
be
ext-real-valued
decreasing
Function
;
let
g
be
ext-real-valued
increasing
Function
;
cluster
f
*
g
->
decreasing
;
coherence
g
*
f
is
decreasing
proof
end;
cluster
g
*
f
->
decreasing
;
coherence
f
*
g
is
decreasing
proof
end;
end;
registration
let
f
be
ext-real-valued
non-increasing
Function
;
let
g
be
ext-real-valued
non-decreasing
Function
;
cluster
f
*
g
->
non-increasing
;
coherence
g
*
f
is
non-increasing
proof
end;
cluster
g
*
f
->
non-increasing
;
coherence
f
*
g
is
non-increasing
proof
end;
end;
registration
let
X
be
ext-real-membered
set
;
cluster
id
X
->
increasing
for
Function
of
X
,
X
;
coherence
for
b
1
being
Function
of
X
,
X
st
b
1
=
id
X
holds
b
1
is
increasing
proof
end;
end;
registration
cluster
non
empty
Relation-like
NAT
-defined
NAT
-valued
Function-like
total
quasi_total
complex-valued
ext-real-valued
real-valued
natural-valued
increasing
for
Element
of
bool
[:
NAT
,
NAT
:]
;
existence
ex
b
1
being
sequence
of
NAT
st
b
1
is
increasing
proof
end;
end;
definition
let
s
be
ManySortedSet
of
NAT
;
mode
subsequence
of
s
->
ManySortedSet
of
NAT
means
:
Def17
:
:: VALUED_0:def 17
ex
N
being
increasing
sequence
of
NAT
st
it
=
s
*
N
;
existence
ex
b
1
being
ManySortedSet
of
NAT
ex
N
being
increasing
sequence
of
NAT
st
b
1
=
s
*
N
proof
end;
end;
::
deftheorem
Def17
defines
subsequence
VALUED_0:def 17 :
for
s
,
b
2
being
ManySortedSet
of
NAT
holds
(
b
2
is
subsequence
of
s
iff ex
N
being
increasing
sequence
of
NAT
st
b
2
=
s
*
N
);
Lm1
:
for
x
being non
empty
set
for
M
being
ManySortedSet
of
NAT
for
s
being
subsequence
of
M
holds
rng
s
c=
rng
M
proof
end;
registration
let
X
be non
empty
set
;
let
s
be
X
-valued
ManySortedSet
of
NAT
;
cluster
->
X
-valued
for
subsequence
of
s
;
coherence
for
b
1
being
subsequence
of
s
holds
b
1
is
X
-valued
proof
end;
end;
definition
let
X
be non
empty
set
;
let
s
be
sequence
of
X
;
:: original:
subsequence
redefine
mode
subsequence
of
s
->
sequence
of
X
;
coherence
for
b
1
being
subsequence
of
s
holds
b
1
is
sequence
of
X
proof
end;
end;
definition
let
X
be non
empty
set
;
let
s
be
sequence
of
X
;
let
k
be
Nat
;
:: original:
^\
redefine
func
s
^\
k
->
subsequence
of
s
;
coherence
s
^\
k
is
subsequence
of
s
proof
end;
end;
theorem
:: VALUED_0:19
for
XX
being non
empty
set
for
ss
being
sequence
of
XX
holds
ss
is
subsequence
of
ss
proof
end;
theorem
:: VALUED_0:20
for
XX
being non
empty
set
for
ss1
,
ss2
,
ss3
being
sequence
of
XX
st
ss1
is
subsequence
of
ss2
&
ss2
is
subsequence
of
ss3
holds
ss1
is
subsequence
of
ss3
proof
end;
:: to be generalized to Function of X,Y
registration
let
X
be
set
;
cluster
Relation-like
NAT
-defined
X
-valued
Function-like
constant
quasi_total
for
Element
of
bool
[:
NAT
,
X
:]
;
existence
ex
b
1
being
sequence
of
X
st
b
1
is
constant
proof
end;
end;
theorem
Th21
:
:: VALUED_0:21
for
XX
being non
empty
set
for
ss
being
sequence
of
XX
for
ss1
being
subsequence
of
ss
holds
rng
ss1
c=
rng
ss
proof
end;
registration
let
X
be non
empty
set
;
let
s
be
constant
sequence
of
X
;
cluster
->
constant
for
subsequence
of
s
;
coherence
for
b
1
being
subsequence
of
s
holds
b
1
is
constant
proof
end;
end;
:: from FRECHET2, 2008.09.08, A.T.
definition
let
X
be non
empty
set
;
let
N
be
increasing
sequence
of
NAT
;
let
s
be
sequence
of
X
;
:: original:
*
redefine
func
s
*
N
->
subsequence
of
s
;
correctness
coherence
N
*
s
is
subsequence
of
s
;
by
Def17
;
end;
theorem
:: VALUED_0:22
for
X
,
Y
being non
empty
set
for
s
,
s1
being
sequence
of
X
for
h
being
PartFunc
of
X
,
Y
st
rng
s
c=
dom
h
&
s1
is
subsequence
of
s
holds
h
/*
s1
is
subsequence
of
h
/*
s
proof
end;
:: to be generalized
registration
let
X
be
with_non-empty_element
set
;
cluster
non
empty
Relation-like
non-empty
NAT
-defined
X
-valued
Function-like
total
quasi_total
for
Element
of
bool
[:
NAT
,
X
:]
;
existence
ex
b
1
being
sequence
of
X
st
b
1
is
non-empty
proof
end;
end;
registration
let
X
be
with_non-empty_element
set
;
let
s
be
non-empty
sequence
of
X
;
cluster
->
non-empty
for
subsequence
of
s
;
coherence
for
b
1
being
subsequence
of
s
holds
b
1
is
non-empty
proof
end;
end;
definition
let
X
be non
empty
set
;
let
s
be
sequence
of
X
;
:: original:
constant
redefine
attr
s
is
constant
means
:: VALUED_0:def 18
ex
x
being
Element
of
X
st
for
n
being
Nat
holds
s
.
n
=
x
;
compatibility
(
s
is
constant
iff ex
x
being
Element
of
X
st
for
n
being
Nat
holds
s
.
n
=
x
)
proof
end;
end;
::
deftheorem
defines
constant
VALUED_0:def 18 :
for
X
being non
empty
set
for
s
being
sequence
of
X
holds
(
s
is
constant
iff ex
x
being
Element
of
X
st
for
n
being
Nat
holds
s
.
n
=
x
);
theorem
Th23
:
:: VALUED_0:23
for
i
,
j
being
Nat
for
X
being
set
for
s
being
constant
sequence
of
X
holds
s
.
i
=
s
.
j
proof
end;
theorem
Th24
:
:: VALUED_0:24
for
X
being non
empty
set
for
s
being
sequence
of
X
st ( for
i
,
j
being
Nat
holds
s
.
i
=
s
.
j
) holds
s
is
V29
()
proof
end;
theorem
:: VALUED_0:25
for
X
being non
empty
set
for
s
being
sequence
of
X
st ( for
i
being
Nat
holds
s
.
i
=
s
.
(
i
+
1
)
) holds
s
is
V29
()
proof
end;
theorem
:: VALUED_0:26
for
X
being non
empty
set
for
s
,
s1
being
sequence
of
X
st
s
is
V29
() &
s1
is
subsequence
of
s
holds
s
=
s1
proof
end;
theorem
Th27
:
:: VALUED_0:27
for
X
,
Y
being non
empty
set
for
s
being
sequence
of
X
for
h
being
PartFunc
of
X
,
Y
for
n
being
Nat
st
rng
s
c=
dom
h
holds
(
h
/*
s
)
^\
n
=
h
/*
(
s
^\
n
)
proof
end;
theorem
Th28
:
:: VALUED_0:28
for
X
being non
empty
set
for
s
being
sequence
of
X
for
n
being
Nat
holds
s
.
n
in
rng
s
proof
end;
theorem
:: VALUED_0:29
for
X
,
Y
being non
empty
set
for
s
being
sequence
of
X
for
h
being
PartFunc
of
X
,
Y
for
n
being
Nat
st
h
is
total
holds
h
/*
(
s
^\
n
)
=
(
h
/*
s
)
^\
n
proof
end;
theorem
Th30
:
:: VALUED_0:30
for
X
,
Y
being non
empty
set
for
s
being
sequence
of
X
for
h
being
PartFunc
of
X
,
Y
st
rng
s
c=
dom
h
holds
h
.:
(
rng
s
)
=
rng
(
h
/*
s
)
proof
end;
theorem
:: VALUED_0:31
for
X
,
Y
being non
empty
set
for
Z
being
set
for
s
being
sequence
of
X
for
h1
being
PartFunc
of
X
,
Y
for
h2
being
PartFunc
of
Y
,
Z
st
rng
s
c=
dom
(
h2
*
h1
)
holds
h2
/*
(
h1
/*
s
)
=
(
h2
*
h1
)
/*
s
proof
end;
definition
let
f
be
ext-real-valued
Function
;
attr
f
is
zeroed
means
:: VALUED_0:def 19
f
.
{}
=
0
;
end;
::
deftheorem
defines
zeroed
VALUED_0:def 19 :
for
f
being
ext-real-valued
Function
holds
(
f
is
zeroed
iff
f
.
{}
=
0
);
:: new, 2009.02.03, A.T.
registration
cluster
Relation-like
COMPLEX
-valued
->
complex-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
COMPLEX
-valued
holds
b
1
is
complex-valued
proof
end;
cluster
Relation-like
ExtREAL
-valued
->
ext-real-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
ExtREAL
-valued
holds
b
1
is
ext-real-valued
proof
end;
cluster
Relation-like
REAL
-valued
->
real-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
REAL
-valued
holds
b
1
is
real-valued
proof
end;
cluster
Relation-like
NAT
-valued
->
natural-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
NAT
-valued
holds
b
1
is
natural-valued
proof
end;
end;
definition
let
s
be
ManySortedSet
of
NAT
;
redefine
attr
s
is
constant
means
:: VALUED_0:def 20
ex
x
being
set
st
for
n
being
Nat
holds
s
.
n
=
x
;
compatibility
(
s
is
constant
iff ex
x
being
set
st
for
n
being
Nat
holds
s
.
n
=
x
)
proof
end;
end;
::
deftheorem
defines
constant
VALUED_0:def 20 :
for
s
being
ManySortedSet
of
NAT
holds
(
s
is
constant
iff ex
x
being
set
st
for
n
being
Nat
holds
s
.
n
=
x
);
theorem
:: VALUED_0:32
for
x
being non
empty
set
for
M
being
ManySortedSet
of
NAT
for
s
being
subsequence
of
M
holds
rng
s
c=
rng
M
by
Lm1
;
registration
let
X
be
set
;
cluster
Relation-like
X
-defined
Function-like
total
natural-valued
for
set
;
existence
ex
b
1
being
ManySortedSet
of
X
st
b
1
is
natural-valued
proof
end;
end;