:: Algebra of Complex Vector Valued Functions
:: by Noboru Endou
::
:: Received August 20, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
begin
::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF COMPLEX NUMBERS
::
definition
let
M
be non
empty
set
;
let
V
be
ComplexNormSpace
;
let
f1
be
PartFunc
of
M
,
COMPLEX
;
let
f2
be
PartFunc
of
M
,
V
;
deffunc
H
1
(
Element
of
M
)
->
Element
of the
U1
of
V
=
(
f1
/.
$1
)
*
(
f2
/.
$1
)
;
defpred
S
1
[
set
]
means
$1
in
(
dom
f1
)
/\
(
dom
f2
)
;
set
X
=
(
dom
f1
)
/\
(
dom
f2
)
;
func
f1
(#)
f2
->
PartFunc
of
M
,
V
means
:
Def1
:
:: VFUNCT_2:def 1
(
dom
it
=
(
dom
f1
)
/\
(
dom
f2
)
& ( for
c
being
Element
of
M
st
c
in
dom
it
holds
it
/.
c
=
(
f1
/.
c
)
*
(
f2
/.
c
)
) );
existence
ex
b
1
being
PartFunc
of
M
,
V
st
(
dom
b
1
=
(
dom
f1
)
/\
(
dom
f2
)
& ( for
c
being
Element
of
M
st
c
in
dom
b
1
holds
b
1
/.
c
=
(
f1
/.
c
)
*
(
f2
/.
c
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
PartFunc
of
M
,
V
st
dom
b
1
=
(
dom
f1
)
/\
(
dom
f2
)
& ( for
c
being
Element
of
M
st
c
in
dom
b
1
holds
b
1
/.
c
=
(
f1
/.
c
)
*
(
f2
/.
c
)
) &
dom
b
2
=
(
dom
f1
)
/\
(
dom
f2
)
& ( for
c
being
Element
of
M
st
c
in
dom
b
2
holds
b
2
/.
c
=
(
f1
/.
c
)
*
(
f2
/.
c
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def1
defines
(#)
VFUNCT_2:def 1 :
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
being
PartFunc
of
M
,
COMPLEX
for
f2
,
b
5
being
PartFunc
of
M
,
V
holds
(
b
5
=
f1
(#)
f2
iff (
dom
b
5
=
(
dom
f1
)
/\
(
dom
f2
)
& ( for
c
being
Element
of
M
st
c
in
dom
b
5
holds
b
5
/.
c
=
(
f1
/.
c
)
*
(
f2
/.
c
)
) ) );
definition
let
X
be non
empty
set
;
let
V
be
ComplexNormSpace
;
let
f
be
PartFunc
of
X
,
V
;
let
z
be
Complex
;
deffunc
H
1
(
Element
of
X
)
->
Element
of the
U1
of
V
=
z
*
(
f
/.
$1
)
;
defpred
S
1
[
set
]
means
$1
in
dom
f
;
set
M
=
dom
f
;
func
z
(#)
f
->
PartFunc
of
X
,
V
means
:
Def2
:
:: VFUNCT_2:def 2
(
dom
it
=
dom
f
& ( for
x
being
Element
of
X
st
x
in
dom
it
holds
it
/.
x
=
z
*
(
f
/.
x
)
) );
existence
ex
b
1
being
PartFunc
of
X
,
V
st
(
dom
b
1
=
dom
f
& ( for
x
being
Element
of
X
st
x
in
dom
b
1
holds
b
1
/.
x
=
z
*
(
f
/.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
PartFunc
of
X
,
V
st
dom
b
1
=
dom
f
& ( for
x
being
Element
of
X
st
x
in
dom
b
1
holds
b
1
/.
x
=
z
*
(
f
/.
x
)
) &
dom
b
2
=
dom
f
& ( for
x
being
Element
of
X
st
x
in
dom
b
2
holds
b
2
/.
x
=
z
*
(
f
/.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def2
defines
(#)
VFUNCT_2:def 2 :
for
X
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
X
,
V
for
z
being
Complex
for
b
5
being
PartFunc
of
X
,
V
holds
(
b
5
=
z
(#)
f
iff (
dom
b
5
=
dom
f
& ( for
x
being
Element
of
X
st
x
in
dom
b
5
holds
b
5
/.
x
=
z
*
(
f
/.
x
)
) ) );
theorem
:: VFUNCT_2:1
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
being
PartFunc
of
M
,
COMPLEX
for
f2
being
PartFunc
of
M
,
V
holds
(
dom
(
f1
(#)
f2
)
)
\
(
(
f1
(#)
f2
)
"
{
(
0.
V
)
}
)
=
(
(
dom
f1
)
\
(
f1
"
{
0
}
)
)
/\
(
(
dom
f2
)
\
(
f2
"
{
(
0.
V
)
}
)
)
proof
end;
theorem
:: VFUNCT_2:2
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
holds
(
||.
f
.||
"
{
0
}
=
f
"
{
(
0.
V
)
}
&
(
-
f
)
"
{
(
0.
V
)
}
=
f
"
{
(
0.
V
)
}
)
proof
end;
theorem
:: VFUNCT_2:3
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
st
z
<>
0c
holds
(
z
(#)
f
)
"
{
(
0.
V
)
}
=
f
"
{
(
0.
V
)
}
proof
end;
::
:: BASIC PROPERTIES OF OPERATIONS
::
theorem
Th4
:
:: VFUNCT_2:4
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
holds
f1
+
f2
=
f2
+
f1
proof
end;
definition
let
M
be non
empty
set
;
let
V
be
ComplexNormSpace
;
let
f1
,
f2
be
PartFunc
of
M
,
V
;
:: original:
+
redefine
func
f1
+
f2
->
Element
of
K6
(
K7
(
M
, the
U1
of
V
));
commutativity
for
f1
,
f2
being
PartFunc
of
M
,
V
holds
f1
+
f2
=
f2
+
f1
by
Th4
;
end;
theorem
:: VFUNCT_2:5
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
,
f3
being
PartFunc
of
M
,
V
holds
(
f1
+
f2
)
+
f3
=
f1
+
(
f2
+
f3
)
proof
end;
theorem
:: VFUNCT_2:6
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
COMPLEX
for
f3
being
PartFunc
of
M
,
V
holds
(
f1
(#)
f2
)
(#)
f3
=
f1
(#)
(
f2
(#)
f3
)
proof
end;
theorem
:: VFUNCT_2:7
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f3
being
PartFunc
of
M
,
V
for
f1
,
f2
being
PartFunc
of
M
,
COMPLEX
holds
(
f1
+
f2
)
(#)
f3
=
(
f1
(#)
f3
)
+
(
f2
(#)
f3
)
proof
end;
theorem
:: VFUNCT_2:8
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
f3
being
PartFunc
of
M
,
COMPLEX
holds
f3
(#)
(
f1
+
f2
)
=
(
f3
(#)
f1
)
+
(
f3
(#)
f2
)
proof
end;
theorem
:: VFUNCT_2:9
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f2
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
for
f1
being
PartFunc
of
M
,
COMPLEX
holds
z
(#)
(
f1
(#)
f2
)
=
(
z
(#)
f1
)
(#)
f2
proof
end;
theorem
:: VFUNCT_2:10
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f2
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
for
f1
being
PartFunc
of
M
,
COMPLEX
holds
z
(#)
(
f1
(#)
f2
)
=
f1
(#)
(
z
(#)
f2
)
proof
end;
theorem
:: VFUNCT_2:11
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f3
being
PartFunc
of
M
,
V
for
f1
,
f2
being
PartFunc
of
M
,
COMPLEX
holds
(
f1
-
f2
)
(#)
f3
=
(
f1
(#)
f3
)
-
(
f2
(#)
f3
)
proof
end;
theorem
:: VFUNCT_2:12
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
f3
being
PartFunc
of
M
,
COMPLEX
holds
(
f3
(#)
f1
)
-
(
f3
(#)
f2
)
=
f3
(#)
(
f1
-
f2
)
proof
end;
theorem
:: VFUNCT_2:13
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
holds
z
(#)
(
f1
+
f2
)
=
(
z
(#)
f1
)
+
(
z
(#)
f2
)
proof
end;
theorem
Th14
:
:: VFUNCT_2:14
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
z1
,
z2
being
Element
of
COMPLEX
holds
(
z1
*
z2
)
(#)
f
=
z1
(#)
(
z2
(#)
f
)
proof
end;
theorem
:: VFUNCT_2:15
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
holds
z
(#)
(
f1
-
f2
)
=
(
z
(#)
f1
)
-
(
z
(#)
f2
)
proof
end;
theorem
:: VFUNCT_2:16
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
holds
f1
-
f2
=
(
-
1r
)
(#)
(
f2
-
f1
)
proof
end;
theorem
:: VFUNCT_2:17
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
,
f3
being
PartFunc
of
M
,
V
holds
f1
-
(
f2
+
f3
)
=
(
f1
-
f2
)
-
f3
proof
end;
theorem
Th18
:
:: VFUNCT_2:18
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
holds
1r
(#)
f
=
f
proof
end;
theorem
:: VFUNCT_2:19
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
,
f3
being
PartFunc
of
M
,
V
holds
f1
-
(
f2
-
f3
)
=
(
f1
-
f2
)
+
f3
proof
end;
theorem
:: VFUNCT_2:20
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
,
f3
being
PartFunc
of
M
,
V
holds
f1
+
(
f2
-
f3
)
=
(
f1
+
f2
)
-
f3
proof
end;
theorem
:: VFUNCT_2:21
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f2
being
PartFunc
of
M
,
V
for
f1
being
PartFunc
of
M
,
COMPLEX
holds
||.
(
f1
(#)
f2
)
.||
=
|.
f1
.|
(#)
||.
f2
.||
proof
end;
theorem
:: VFUNCT_2:22
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
holds
||.
(
z
(#)
f
)
.||
=
|.
z
.|
(#)
||.
f
.||
proof
end;
theorem
Th23
:
:: VFUNCT_2:23
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
holds
-
f
=
(
-
1r
)
(#)
f
proof
end;
theorem
Th24
:
:: VFUNCT_2:24
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
holds
-
(
-
f
)
=
f
proof
end;
theorem
Th25
:
:: VFUNCT_2:25
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
holds
f1
-
f2
=
f1
+
(
-
f2
)
proof
end;
theorem
:: VFUNCT_2:26
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
holds
f1
-
(
-
f2
)
=
f1
+
f2
proof
end;
theorem
Th27
:
:: VFUNCT_2:27
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
X
being
set
holds
(
(
f1
+
f2
)
|
X
=
(
f1
|
X
)
+
(
f2
|
X
)
&
(
f1
+
f2
)
|
X
=
(
f1
|
X
)
+
f2
&
(
f1
+
f2
)
|
X
=
f1
+
(
f2
|
X
)
)
proof
end;
theorem
:: VFUNCT_2:28
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f2
being
PartFunc
of
M
,
V
for
X
being
set
for
f1
being
PartFunc
of
M
,
COMPLEX
holds
(
(
f1
(#)
f2
)
|
X
=
(
f1
|
X
)
(#)
(
f2
|
X
)
&
(
f1
(#)
f2
)
|
X
=
(
f1
|
X
)
(#)
f2
&
(
f1
(#)
f2
)
|
X
=
f1
(#)
(
f2
|
X
)
)
proof
end;
theorem
Th29
:
:: VFUNCT_2:29
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
X
being
set
holds
(
(
-
f
)
|
X
=
-
(
f
|
X
)
&
||.
f
.||
|
X
=
||.
(
f
|
X
)
.||
)
proof
end;
theorem
:: VFUNCT_2:30
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
X
being
set
holds
(
(
f1
-
f2
)
|
X
=
(
f1
|
X
)
-
(
f2
|
X
)
&
(
f1
-
f2
)
|
X
=
(
f1
|
X
)
-
f2
&
(
f1
-
f2
)
|
X
=
f1
-
(
f2
|
X
)
)
proof
end;
theorem
:: VFUNCT_2:31
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
for
X
being
set
holds
(
z
(#)
f
)
|
X
=
z
(#)
(
f
|
X
)
proof
end;
::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO COMPLEX
::
theorem
Th32
:
:: VFUNCT_2:32
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
holds
( (
f1
is
total
&
f2
is
total
implies
f1
+
f2
is
total
) & (
f1
+
f2
is
total
implies (
f1
is
total
&
f2
is
total
) ) & (
f1
is
total
&
f2
is
total
implies
f1
-
f2
is
total
) & (
f1
-
f2
is
total
implies (
f1
is
total
&
f2
is
total
) ) )
proof
end;
theorem
Th33
:
:: VFUNCT_2:33
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f2
being
PartFunc
of
M
,
V
for
f1
being
PartFunc
of
M
,
COMPLEX
holds
( (
f1
is
total
&
f2
is
total
) iff
f1
(#)
f2
is
total
)
proof
end;
theorem
Th34
:
:: VFUNCT_2:34
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
holds
(
f
is
total
iff
z
(#)
f
is
total
)
proof
end;
theorem
Th35
:
:: VFUNCT_2:35
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
holds
(
f
is
total
iff
-
f
is
total
)
proof
end;
theorem
Th36
:
:: VFUNCT_2:36
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
holds
(
f
is
total
iff
||.
f
.||
is
total
)
proof
end;
theorem
:: VFUNCT_2:37
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
x
being
Element
of
M
st
f1
is
total
&
f2
is
total
holds
(
(
f1
+
f2
)
/.
x
=
(
f1
/.
x
)
+
(
f2
/.
x
)
&
(
f1
-
f2
)
/.
x
=
(
f1
/.
x
)
-
(
f2
/.
x
)
)
proof
end;
theorem
:: VFUNCT_2:38
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f2
being
PartFunc
of
M
,
V
for
f1
being
PartFunc
of
M
,
COMPLEX
for
x
being
Element
of
M
st
f1
is
total
&
f2
is
total
holds
(
f1
(#)
f2
)
/.
x
=
(
f1
/.
x
)
*
(
f2
/.
x
)
proof
end;
theorem
:: VFUNCT_2:39
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
for
x
being
Element
of
M
st
f
is
total
holds
(
z
(#)
f
)
/.
x
=
z
*
(
f
/.
x
)
proof
end;
theorem
:: VFUNCT_2:40
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
x
being
Element
of
M
st
f
is
total
holds
(
(
-
f
)
/.
x
=
-
(
f
/.
x
)
&
||.
f
.||
.
x
=
||.
(
f
/.
x
)
.||
)
proof
end;
::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS
:: FROM A DOMAIN TO A NORMED COMPLEX SPACE
::
definition
let
M
be non
empty
set
;
let
V
be
ComplexNormSpace
;
let
f
be
PartFunc
of
M
,
V
;
let
Y
be
set
;
pred
f
is_bounded_on
Y
means
:
Def3
:
:: VFUNCT_2:def 3
ex
r
being
Real
st
for
x
being
Element
of
M
st
x
in
Y
/\
(
dom
f
)
holds
||.
(
f
/.
x
)
.||
<=
r
;
end;
::
deftheorem
Def3
defines
is_bounded_on
VFUNCT_2:def 3 :
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
Y
being
set
holds
(
f
is_bounded_on
Y
iff ex
r
being
Real
st
for
x
being
Element
of
M
st
x
in
Y
/\
(
dom
f
)
holds
||.
(
f
/.
x
)
.||
<=
r
);
theorem
:: VFUNCT_2:41
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
Y
,
X
being
set
st
Y
c=
X
&
f
is_bounded_on
X
holds
f
is_bounded_on
Y
proof
end;
theorem
:: VFUNCT_2:42
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
X
being
set
st
X
misses
dom
f
holds
f
is_bounded_on
X
proof
end;
theorem
:: VFUNCT_2:43
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
Y
being
set
holds
0c
(#)
f
is_bounded_on
Y
proof
end;
theorem
Th44
:
:: VFUNCT_2:44
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
for
Y
being
set
st
f
is_bounded_on
Y
holds
z
(#)
f
is_bounded_on
Y
proof
end;
theorem
Th45
:
:: VFUNCT_2:45
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
Y
being
set
st
f
is_bounded_on
Y
holds
(
||.
f
.||
|
Y
is
bounded
&
-
f
is_bounded_on
Y
)
proof
end;
theorem
Th46
:
:: VFUNCT_2:46
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
X
,
Y
being
set
st
f1
is_bounded_on
X
&
f2
is_bounded_on
Y
holds
f1
+
f2
is_bounded_on
X
/\
Y
proof
end;
theorem
:: VFUNCT_2:47
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f2
being
PartFunc
of
M
,
V
for
X
,
Y
being
set
for
f1
being
PartFunc
of
M
,
COMPLEX
st
f1
|
X
is
bounded
&
f2
is_bounded_on
Y
holds
f1
(#)
f2
is_bounded_on
X
/\
Y
proof
end;
theorem
:: VFUNCT_2:48
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
X
,
Y
being
set
st
f1
is_bounded_on
X
&
f2
is_bounded_on
Y
holds
f1
-
f2
is_bounded_on
X
/\
Y
proof
end;
theorem
:: VFUNCT_2:49
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
X
,
Y
being
set
st
f
is_bounded_on
X
&
f
is_bounded_on
Y
holds
f
is_bounded_on
X
\/
Y
proof
end;
theorem
:: VFUNCT_2:50
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
X
,
Y
being
set
st
f1
|
X
is
constant
&
f2
|
Y
is
constant
holds
(
(
f1
+
f2
)
|
(
X
/\
Y
)
is
constant
&
(
f1
-
f2
)
|
(
X
/\
Y
)
is
constant
)
proof
end;
theorem
:: VFUNCT_2:51
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f2
being
PartFunc
of
M
,
V
for
X
,
Y
being
set
for
f1
being
PartFunc
of
M
,
COMPLEX
st
f1
|
X
is
constant
&
f2
|
Y
is
constant
holds
(
f1
(#)
f2
)
|
(
X
/\
Y
)
is
constant
proof
end;
theorem
Th52
:
:: VFUNCT_2:52
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
z
being
Element
of
COMPLEX
for
Y
being
set
st
f
|
Y
is
constant
holds
(
z
(#)
f
)
|
Y
is
constant
proof
end;
theorem
Th53
:
:: VFUNCT_2:53
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
Y
being
set
st
f
|
Y
is
constant
holds
(
||.
f
.||
|
Y
is
constant
&
(
-
f
)
|
Y
is
constant
)
proof
end;
theorem
Th54
:
:: VFUNCT_2:54
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
Y
being
set
st
f
|
Y
is
constant
holds
f
is_bounded_on
Y
proof
end;
theorem
:: VFUNCT_2:55
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f
being
PartFunc
of
M
,
V
for
Y
being
set
st
f
|
Y
is
constant
holds
( ( for
z
being
Element
of
COMPLEX
holds
z
(#)
f
is_bounded_on
Y
) &
-
f
is_bounded_on
Y
&
||.
f
.||
|
Y
is
bounded
)
proof
end;
theorem
:: VFUNCT_2:56
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
X
,
Y
being
set
st
f1
is_bounded_on
X
&
f2
|
Y
is
constant
holds
f1
+
f2
is_bounded_on
X
/\
Y
proof
end;
theorem
:: VFUNCT_2:57
for
M
being non
empty
set
for
V
being
ComplexNormSpace
for
f1
,
f2
being
PartFunc
of
M
,
V
for
X
,
Y
being
set
st
f1
is_bounded_on
X
&
f2
|
Y
is
constant
holds
(
f1
-
f2
is_bounded_on
X
/\
Y
&
f2
-
f1
is_bounded_on
X
/\
Y
)
proof
end;
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF COMPLEX NUMBERS
::