:: Arithmetic Operations on Functions from Sets into Functional Sets
:: by Artur Korni{\l}owicz
::
:: Received October 15, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users
begin
Lm1
:
now
:: thesis:
for
X1
,
X2
,
X3
being
set
holds
X1
/\
(
X2
/\
X3
)
=
(
X1
/\
X2
)
/\
(
X1
/\
X3
)
let
X1
,
X2
,
X3
be
set
;
:: thesis:
X1
/\
(
X2
/\
X3
)
=
(
X1
/\
X2
)
/\
(
X1
/\
X3
)
thus
X1
/\
(
X2
/\
X3
)
=
(
(
X1
/\
X1
)
/\
X2
)
/\
X3
by
XBOOLE_1:16
.=
(
X1
/\
(
X1
/\
X2
)
)
/\
X3
by
XBOOLE_1:16
.=
(
X1
/\
X2
)
/\
(
X1
/\
X3
)
by
XBOOLE_1:16
;
:: thesis:
verum
end;
definition
let
Y
be
functional
set
;
func
DOMS
Y
->
set
equals
:: VALUED_2:def 1
union
{
(
dom
f
)
where
f
is
Element
of
Y
: verum
}
;
coherence
union
{
(
dom
f
)
where
f
is
Element
of
Y
: verum
}
is
set
;
end;
::
deftheorem
defines
DOMS
VALUED_2:def 1 :
for
Y
being
functional
set
holds
DOMS
Y
=
union
{
(
dom
f
)
where
f
is
Element
of
Y
: verum
}
;
definition
let
X
be
set
;
attr
X
is
complex-functions-membered
means
:
Def2
:
:: VALUED_2:def 2
for
x
being
set
st
x
in
X
holds
x
is
complex-valued
Function
;
end;
::
deftheorem
Def2
defines
complex-functions-membered
VALUED_2:def 2 :
for
X
being
set
holds
(
X
is
complex-functions-membered
iff for
x
being
set
st
x
in
X
holds
x
is
complex-valued
Function
);
definition
let
X
be
set
;
attr
X
is
ext-real-functions-membered
means
:
Def3
:
:: VALUED_2:def 3
for
x
being
set
st
x
in
X
holds
x
is
ext-real-valued
Function
;
end;
::
deftheorem
Def3
defines
ext-real-functions-membered
VALUED_2:def 3 :
for
X
being
set
holds
(
X
is
ext-real-functions-membered
iff for
x
being
set
st
x
in
X
holds
x
is
ext-real-valued
Function
);
definition
let
X
be
set
;
attr
X
is
real-functions-membered
means
:
Def4
:
:: VALUED_2:def 4
for
x
being
set
st
x
in
X
holds
x
is
real-valued
Function
;
end;
::
deftheorem
Def4
defines
real-functions-membered
VALUED_2:def 4 :
for
X
being
set
holds
(
X
is
real-functions-membered
iff for
x
being
set
st
x
in
X
holds
x
is
real-valued
Function
);
definition
let
X
be
set
;
attr
X
is
rational-functions-membered
means
:
Def5
:
:: VALUED_2:def 5
for
x
being
set
st
x
in
X
holds
x
is
RAT
-valued
Function
;
end;
::
deftheorem
Def5
defines
rational-functions-membered
VALUED_2:def 5 :
for
X
being
set
holds
(
X
is
rational-functions-membered
iff for
x
being
set
st
x
in
X
holds
x
is
RAT
-valued
Function
);
definition
let
X
be
set
;
attr
X
is
integer-functions-membered
means
:
Def6
:
:: VALUED_2:def 6
for
x
being
set
st
x
in
X
holds
x
is
INT
-valued
Function
;
end;
::
deftheorem
Def6
defines
integer-functions-membered
VALUED_2:def 6 :
for
X
being
set
holds
(
X
is
integer-functions-membered
iff for
x
being
set
st
x
in
X
holds
x
is
INT
-valued
Function
);
definition
let
X
be
set
;
attr
X
is
natural-functions-membered
means
:
Def7
:
:: VALUED_2:def 7
for
x
being
set
st
x
in
X
holds
x
is
natural-valued
Function
;
end;
::
deftheorem
Def7
defines
natural-functions-membered
VALUED_2:def 7 :
for
X
being
set
holds
(
X
is
natural-functions-membered
iff for
x
being
set
st
x
in
X
holds
x
is
natural-valued
Function
);
registration
cluster
natural-functions-membered
->
integer-functions-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
natural-functions-membered
holds
b
1
is
integer-functions-membered
proof
end;
cluster
integer-functions-membered
->
rational-functions-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
integer-functions-membered
holds
b
1
is
rational-functions-membered
proof
end;
cluster
rational-functions-membered
->
real-functions-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
rational-functions-membered
holds
b
1
is
real-functions-membered
proof
end;
cluster
real-functions-membered
->
complex-functions-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
real-functions-membered
holds
b
1
is
complex-functions-membered
proof
end;
cluster
real-functions-membered
->
ext-real-functions-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
real-functions-membered
holds
b
1
is
ext-real-functions-membered
proof
end;
end;
registration
cluster
empty
->
natural-functions-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
empty
holds
b
1
is
natural-functions-membered
proof
end;
end;
registration
let
f
be
complex-valued
Function
;
cluster
{
f
}
->
complex-functions-membered
;
coherence
{
f
}
is
complex-functions-membered
proof
end;
end;
registration
cluster
complex-functions-membered
->
functional
for
set
;
coherence
for
b
1
being
set
st
b
1
is
complex-functions-membered
holds
b
1
is
functional
proof
end;
cluster
ext-real-functions-membered
->
functional
for
set
;
coherence
for
b
1
being
set
st
b
1
is
ext-real-functions-membered
holds
b
1
is
functional
proof
end;
end;
set
ff
= the
natural-valued
Function
;
registration
cluster
non
empty
natural-functions-membered
for
set
;
existence
ex
b
1
being
set
st
(
b
1
is
natural-functions-membered
& not
b
1
is
empty
)
proof
end;
end;
registration
let
X
be
complex-functions-membered
set
;
cluster
->
complex-functions-membered
for
Element
of
K19
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
complex-functions-membered
proof
end;
end;
registration
let
X
be
ext-real-functions-membered
set
;
cluster
->
ext-real-functions-membered
for
Element
of
K19
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
ext-real-functions-membered
proof
end;
end;
registration
let
X
be
real-functions-membered
set
;
cluster
->
real-functions-membered
for
Element
of
K19
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
real-functions-membered
proof
end;
end;
registration
let
X
be
rational-functions-membered
set
;
cluster
->
rational-functions-membered
for
Element
of
K19
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
rational-functions-membered
proof
end;
end;
registration
let
X
be
integer-functions-membered
set
;
cluster
->
integer-functions-membered
for
Element
of
K19
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
integer-functions-membered
proof
end;
end;
registration
let
X
be
natural-functions-membered
set
;
cluster
->
natural-functions-membered
for
Element
of
K19
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
natural-functions-membered
proof
end;
end;
definition
set
A
=
COMPLEX
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
PartFunc
of
D
,
COMPLEX
;
func
C_PFuncs
D
->
set
means
:
Def8
:
:: VALUED_2:def 8
for
f
being
set
holds
(
f
in
it
iff
f
is
PartFunc
of
D
,
COMPLEX
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
COMPLEX
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
COMPLEX
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
COMPLEX
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def8
defines
C_PFuncs
VALUED_2:def 8 :
for
D
,
b
2
being
set
holds
(
b
2
=
C_PFuncs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
COMPLEX
) );
definition
set
A
=
COMPLEX
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
Function
of
D
,
COMPLEX
;
func
C_Funcs
D
->
set
means
:
Def9
:
:: VALUED_2:def 9
for
f
being
set
holds
(
f
in
it
iff
f
is
Function
of
D
,
COMPLEX
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
COMPLEX
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
COMPLEX
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
COMPLEX
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def9
defines
C_Funcs
VALUED_2:def 9 :
for
D
,
b
2
being
set
holds
(
b
2
=
C_Funcs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
COMPLEX
) );
definition
set
A
=
ExtREAL
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
PartFunc
of
D
,
ExtREAL
;
func
E_PFuncs
D
->
set
means
:
Def10
:
:: VALUED_2:def 10
for
f
being
set
holds
(
f
in
it
iff
f
is
PartFunc
of
D
,
ExtREAL
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
ExtREAL
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
ExtREAL
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
ExtREAL
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def10
defines
E_PFuncs
VALUED_2:def 10 :
for
D
,
b
2
being
set
holds
(
b
2
=
E_PFuncs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
ExtREAL
) );
definition
set
A
=
ExtREAL
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
Function
of
D
,
ExtREAL
;
func
E_Funcs
D
->
set
means
:
Def11
:
:: VALUED_2:def 11
for
f
being
set
holds
(
f
in
it
iff
f
is
Function
of
D
,
ExtREAL
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
ExtREAL
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
ExtREAL
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
ExtREAL
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def11
defines
E_Funcs
VALUED_2:def 11 :
for
D
,
b
2
being
set
holds
(
b
2
=
E_Funcs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
ExtREAL
) );
definition
set
A
=
REAL
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
PartFunc
of
D
,
REAL
;
func
R_PFuncs
D
->
set
means
:
Def12
:
:: VALUED_2:def 12
for
f
being
set
holds
(
f
in
it
iff
f
is
PartFunc
of
D
,
REAL
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
REAL
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
REAL
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
REAL
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def12
defines
R_PFuncs
VALUED_2:def 12 :
for
D
,
b
2
being
set
holds
(
b
2
=
R_PFuncs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
REAL
) );
definition
set
A
=
REAL
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
Function
of
D
,
REAL
;
func
R_Funcs
D
->
set
means
:
Def13
:
:: VALUED_2:def 13
for
f
being
set
holds
(
f
in
it
iff
f
is
Function
of
D
,
REAL
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
REAL
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
REAL
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
REAL
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def13
defines
R_Funcs
VALUED_2:def 13 :
for
D
,
b
2
being
set
holds
(
b
2
=
R_Funcs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
REAL
) );
definition
set
A
=
RAT
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
PartFunc
of
D
,
RAT
;
func
Q_PFuncs
D
->
set
means
:
Def14
:
:: VALUED_2:def 14
for
f
being
set
holds
(
f
in
it
iff
f
is
PartFunc
of
D
,
RAT
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
RAT
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
RAT
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
RAT
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def14
defines
Q_PFuncs
VALUED_2:def 14 :
for
D
,
b
2
being
set
holds
(
b
2
=
Q_PFuncs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
RAT
) );
definition
set
A
=
RAT
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
Function
of
D
,
RAT
;
func
Q_Funcs
D
->
set
means
:
Def15
:
:: VALUED_2:def 15
for
f
being
set
holds
(
f
in
it
iff
f
is
Function
of
D
,
RAT
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
RAT
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
RAT
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
RAT
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def15
defines
Q_Funcs
VALUED_2:def 15 :
for
D
,
b
2
being
set
holds
(
b
2
=
Q_Funcs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
RAT
) );
definition
set
A
=
INT
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
PartFunc
of
D
,
INT
;
func
I_PFuncs
D
->
set
means
:
Def16
:
:: VALUED_2:def 16
for
f
being
set
holds
(
f
in
it
iff
f
is
PartFunc
of
D
,
INT
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
INT
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
INT
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
INT
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def16
defines
I_PFuncs
VALUED_2:def 16 :
for
D
,
b
2
being
set
holds
(
b
2
=
I_PFuncs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
INT
) );
definition
set
A
=
INT
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
Function
of
D
,
INT
;
func
I_Funcs
D
->
set
means
:
Def17
:
:: VALUED_2:def 17
for
f
being
set
holds
(
f
in
it
iff
f
is
Function
of
D
,
INT
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
INT
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
INT
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
INT
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def17
defines
I_Funcs
VALUED_2:def 17 :
for
D
,
b
2
being
set
holds
(
b
2
=
I_Funcs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
INT
) );
definition
set
A
=
NAT
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
PartFunc
of
D
,
NAT
;
func
N_PFuncs
D
->
set
means
:
Def18
:
:: VALUED_2:def 18
for
f
being
set
holds
(
f
in
it
iff
f
is
PartFunc
of
D
,
NAT
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
NAT
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
PartFunc
of
D
,
NAT
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
NAT
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def18
defines
N_PFuncs
VALUED_2:def 18 :
for
D
,
b
2
being
set
holds
(
b
2
=
N_PFuncs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
PartFunc
of
D
,
NAT
) );
definition
set
A
=
NAT
;
let
D
be
set
;
defpred
S
1
[
set
]
means
$1 is
Function
of
D
,
NAT
;
func
N_Funcs
D
->
set
means
:
Def19
:
:: VALUED_2:def 19
for
f
being
set
holds
(
f
in
it
iff
f
is
Function
of
D
,
NAT
);
existence
ex
b
1
being
set
st
for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
NAT
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
f
being
set
holds
(
f
in
b
1
iff
f
is
Function
of
D
,
NAT
) ) & ( for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
NAT
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def19
defines
N_Funcs
VALUED_2:def 19 :
for
D
,
b
2
being
set
holds
(
b
2
=
N_Funcs
D
iff for
f
being
set
holds
(
f
in
b
2
iff
f
is
Function
of
D
,
NAT
) );
theorem
Th1
:
:: VALUED_2:1
for
X
being
set
holds
C_Funcs
X
is
Subset
of
(
C_PFuncs
X
)
proof
end;
theorem
Th2
:
:: VALUED_2:2
for
X
being
set
holds
E_Funcs
X
is
Subset
of
(
E_PFuncs
X
)
proof
end;
theorem
Th3
:
:: VALUED_2:3
for
X
being
set
holds
R_Funcs
X
is
Subset
of
(
R_PFuncs
X
)
proof
end;
theorem
Th4
:
:: VALUED_2:4
for
X
being
set
holds
Q_Funcs
X
is
Subset
of
(
Q_PFuncs
X
)
proof
end;
theorem
Th5
:
:: VALUED_2:5
for
X
being
set
holds
I_Funcs
X
is
Subset
of
(
I_PFuncs
X
)
proof
end;
theorem
Th6
:
:: VALUED_2:6
for
X
being
set
holds
N_Funcs
X
is
Subset
of
(
N_PFuncs
X
)
proof
end;
registration
let
X
be
set
;
cluster
C_PFuncs
X
->
complex-functions-membered
;
coherence
C_PFuncs
X
is
complex-functions-membered
proof
end;
cluster
C_Funcs
X
->
complex-functions-membered
;
coherence
C_Funcs
X
is
complex-functions-membered
proof
end;
cluster
E_PFuncs
X
->
ext-real-functions-membered
;
coherence
E_PFuncs
X
is
ext-real-functions-membered
proof
end;
cluster
E_Funcs
X
->
ext-real-functions-membered
;
coherence
E_Funcs
X
is
ext-real-functions-membered
proof
end;
cluster
R_PFuncs
X
->
real-functions-membered
;
coherence
R_PFuncs
X
is
real-functions-membered
proof
end;
cluster
R_Funcs
X
->
real-functions-membered
;
coherence
R_Funcs
X
is
real-functions-membered
proof
end;
cluster
Q_PFuncs
X
->
rational-functions-membered
;
coherence
Q_PFuncs
X
is
rational-functions-membered
proof
end;
cluster
Q_Funcs
X
->
rational-functions-membered
;
coherence
Q_Funcs
X
is
rational-functions-membered
proof
end;
cluster
I_PFuncs
X
->
integer-functions-membered
;
coherence
I_PFuncs
X
is
integer-functions-membered
proof
end;
cluster
I_Funcs
X
->
integer-functions-membered
;
coherence
I_Funcs
X
is
integer-functions-membered
proof
end;
cluster
N_PFuncs
X
->
natural-functions-membered
;
coherence
N_PFuncs
X
is
natural-functions-membered
proof
end;
cluster
N_Funcs
X
->
natural-functions-membered
;
coherence
N_Funcs
X
is
natural-functions-membered
proof
end;
end;
registration
let
X
be
complex-functions-membered
set
;
cluster
->
complex-valued
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
complex-valued
proof
end;
end;
registration
let
X
be
ext-real-functions-membered
set
;
cluster
->
ext-real-valued
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
ext-real-valued
proof
end;
end;
registration
let
X
be
real-functions-membered
set
;
cluster
->
real-valued
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
real-valued
proof
end;
end;
registration
let
X
be
rational-functions-membered
set
;
cluster
->
RAT
-valued
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
RAT
-valued
proof
end;
end;
registration
let
X
be
integer-functions-membered
set
;
cluster
->
INT
-valued
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
INT
-valued
proof
end;
end;
registration
let
X
be
natural-functions-membered
set
;
cluster
->
natural-valued
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
natural-valued
proof
end;
end;
registration
let
X
,
x
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
cluster
f
.
x
->
Relation-like
Function-like
;
coherence
(
f
.
x
is
Function-like
&
f
.
x
is
Relation-like
)
;
end;
registration
let
X
,
x
be
set
;
let
Y
be
ext-real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
cluster
f
.
x
->
Relation-like
Function-like
;
coherence
(
f
.
x
is
Function-like
&
f
.
x
is
Relation-like
)
;
end;
registration
let
X
,
x
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
cluster
f
.
x
->
complex-valued
;
coherence
f
.
x
is
complex-valued
proof
end;
end;
registration
let
X
,
x
be
set
;
let
Y
be
ext-real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
cluster
f
.
x
->
ext-real-valued
;
coherence
f
.
x
is
ext-real-valued
proof
end;
end;
registration
let
X
,
x
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
cluster
f
.
x
->
real-valued
;
coherence
f
.
x
is
real-valued
proof
end;
end;
registration
let
X
,
x
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
cluster
f
.
x
->
RAT
-valued
;
coherence
f
.
x
is
RAT
-valued
proof
end;
end;
registration
let
X
,
x
be
set
;
let
Y
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
cluster
f
.
x
->
INT
-valued
;
coherence
f
.
x
is
INT
-valued
proof
end;
end;
registration
let
X
,
x
be
set
;
let
Y
be
natural-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
cluster
f
.
x
->
natural-valued
;
coherence
f
.
x
is
natural-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
complex-membered
set
;
cluster
PFuncs
(
X
,
Y
)
->
complex-functions-membered
;
coherence
PFuncs
(
X
,
Y
) is
complex-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
ext-real-membered
set
;
cluster
PFuncs
(
X
,
Y
)
->
ext-real-functions-membered
;
coherence
PFuncs
(
X
,
Y
) is
ext-real-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
real-membered
set
;
cluster
PFuncs
(
X
,
Y
)
->
real-functions-membered
;
coherence
PFuncs
(
X
,
Y
) is
real-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
rational-membered
set
;
cluster
PFuncs
(
X
,
Y
)
->
rational-functions-membered
;
coherence
PFuncs
(
X
,
Y
) is
rational-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
integer-membered
set
;
cluster
PFuncs
(
X
,
Y
)
->
integer-functions-membered
;
coherence
PFuncs
(
X
,
Y
) is
integer-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
natural-membered
set
;
cluster
PFuncs
(
X
,
Y
)
->
natural-functions-membered
;
coherence
PFuncs
(
X
,
Y
) is
natural-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
complex-membered
set
;
cluster
Funcs
(
X
,
Y
)
->
complex-functions-membered
;
coherence
Funcs
(
X
,
Y
) is
complex-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
ext-real-membered
set
;
cluster
Funcs
(
X
,
Y
)
->
ext-real-functions-membered
;
coherence
Funcs
(
X
,
Y
) is
ext-real-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
real-membered
set
;
cluster
Funcs
(
X
,
Y
)
->
real-functions-membered
;
coherence
Funcs
(
X
,
Y
) is
real-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
rational-membered
set
;
cluster
Funcs
(
X
,
Y
)
->
rational-functions-membered
;
coherence
Funcs
(
X
,
Y
) is
rational-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
integer-membered
set
;
cluster
Funcs
(
X
,
Y
)
->
integer-functions-membered
;
coherence
Funcs
(
X
,
Y
) is
integer-functions-membered
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
natural-membered
set
;
cluster
Funcs
(
X
,
Y
)
->
natural-functions-membered
;
coherence
Funcs
(
X
,
Y
) is
natural-functions-membered
proof
end;
end;
definition
let
R
be
Relation
;
attr
R
is
complex-functions-valued
means
:
Def20
:
:: VALUED_2:def 20
rng
R
is
complex-functions-membered
;
attr
R
is
ext-real-functions-valued
means
:
Def21
:
:: VALUED_2:def 21
rng
R
is
ext-real-functions-membered
;
attr
R
is
real-functions-valued
means
:
Def22
:
:: VALUED_2:def 22
rng
R
is
real-functions-membered
;
attr
R
is
rational-functions-valued
means
:
Def23
:
:: VALUED_2:def 23
rng
R
is
rational-functions-membered
;
attr
R
is
integer-functions-valued
means
:
Def24
:
:: VALUED_2:def 24
rng
R
is
integer-functions-membered
;
attr
R
is
natural-functions-valued
means
:
Def25
:
:: VALUED_2:def 25
rng
R
is
natural-functions-membered
;
end;
::
deftheorem
Def20
defines
complex-functions-valued
VALUED_2:def 20 :
for
R
being
Relation
holds
(
R
is
complex-functions-valued
iff
rng
R
is
complex-functions-membered
);
::
deftheorem
Def21
defines
ext-real-functions-valued
VALUED_2:def 21 :
for
R
being
Relation
holds
(
R
is
ext-real-functions-valued
iff
rng
R
is
ext-real-functions-membered
);
::
deftheorem
Def22
defines
real-functions-valued
VALUED_2:def 22 :
for
R
being
Relation
holds
(
R
is
real-functions-valued
iff
rng
R
is
real-functions-membered
);
::
deftheorem
Def23
defines
rational-functions-valued
VALUED_2:def 23 :
for
R
being
Relation
holds
(
R
is
rational-functions-valued
iff
rng
R
is
rational-functions-membered
);
::
deftheorem
Def24
defines
integer-functions-valued
VALUED_2:def 24 :
for
R
being
Relation
holds
(
R
is
integer-functions-valued
iff
rng
R
is
integer-functions-membered
);
::
deftheorem
Def25
defines
natural-functions-valued
VALUED_2:def 25 :
for
R
being
Relation
holds
(
R
is
natural-functions-valued
iff
rng
R
is
natural-functions-membered
);
registration
let
Y
be
complex-functions-membered
set
;
cluster
Relation-like
Y
-valued
Function-like
->
Y
-valued
complex-functions-valued
for
set
;
coherence
for
b
1
being
Y
-valued
Function
holds
b
1
is
complex-functions-valued
proof
end;
end;
definition
let
f
be
Function
;
redefine
attr
f
is
complex-functions-valued
means
:: VALUED_2:def 26
for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
complex-valued
Function
;
compatibility
(
f
is
complex-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
complex-valued
Function
)
proof
end;
redefine
attr
f
is
ext-real-functions-valued
means
:: VALUED_2:def 27
for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
ext-real-valued
Function
;
compatibility
(
f
is
ext-real-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
ext-real-valued
Function
)
proof
end;
redefine
attr
f
is
real-functions-valued
means
:: VALUED_2:def 28
for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
real-valued
Function
;
compatibility
(
f
is
real-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
real-valued
Function
)
proof
end;
redefine
attr
f
is
rational-functions-valued
means
:: VALUED_2:def 29
for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
RAT
-valued
Function
;
compatibility
(
f
is
rational-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
RAT
-valued
Function
)
proof
end;
redefine
attr
f
is
integer-functions-valued
means
:: VALUED_2:def 30
for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
INT
-valued
Function
;
compatibility
(
f
is
integer-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
INT
-valued
Function
)
proof
end;
redefine
attr
f
is
natural-functions-valued
means
:: VALUED_2:def 31
for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
natural-valued
Function
;
compatibility
(
f
is
natural-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
natural-valued
Function
)
proof
end;
end;
::
deftheorem
defines
complex-functions-valued
VALUED_2:def 26 :
for
f
being
Function
holds
(
f
is
complex-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
complex-valued
Function
);
::
deftheorem
defines
ext-real-functions-valued
VALUED_2:def 27 :
for
f
being
Function
holds
(
f
is
ext-real-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
ext-real-valued
Function
);
::
deftheorem
defines
real-functions-valued
VALUED_2:def 28 :
for
f
being
Function
holds
(
f
is
real-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
real-valued
Function
);
::
deftheorem
defines
rational-functions-valued
VALUED_2:def 29 :
for
f
being
Function
holds
(
f
is
rational-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
RAT
-valued
Function
);
::
deftheorem
defines
integer-functions-valued
VALUED_2:def 30 :
for
f
being
Function
holds
(
f
is
integer-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
INT
-valued
Function
);
::
deftheorem
defines
natural-functions-valued
VALUED_2:def 31 :
for
f
being
Function
holds
(
f
is
natural-functions-valued
iff for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
natural-valued
Function
);
registration
cluster
Relation-like
natural-functions-valued
->
integer-functions-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
natural-functions-valued
holds
b
1
is
integer-functions-valued
proof
end;
cluster
Relation-like
integer-functions-valued
->
rational-functions-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
integer-functions-valued
holds
b
1
is
rational-functions-valued
proof
end;
cluster
Relation-like
rational-functions-valued
->
real-functions-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
rational-functions-valued
holds
b
1
is
real-functions-valued
proof
end;
cluster
Relation-like
real-functions-valued
->
ext-real-functions-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
real-functions-valued
holds
b
1
is
ext-real-functions-valued
proof
end;
cluster
Relation-like
real-functions-valued
->
complex-functions-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
real-functions-valued
holds
b
1
is
complex-functions-valued
proof
end;
end;
registration
cluster
Relation-like
empty
->
natural-functions-valued
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
empty
holds
b
1
is
natural-functions-valued
proof
end;
end;
registration
cluster
Relation-like
Function-like
natural-functions-valued
for
set
;
existence
ex
b
1
being
Function
st
b
1
is
natural-functions-valued
proof
end;
end;
registration
let
R
be
complex-functions-valued
Relation
;
cluster
rng
R
->
complex-functions-membered
;
coherence
rng
R
is
complex-functions-membered
by
Def20
;
end;
registration
let
R
be
ext-real-functions-valued
Relation
;
cluster
rng
R
->
ext-real-functions-membered
;
coherence
rng
R
is
ext-real-functions-membered
by
Def21
;
end;
registration
let
R
be
real-functions-valued
Relation
;
cluster
rng
R
->
real-functions-membered
;
coherence
rng
R
is
real-functions-membered
by
Def22
;
end;
registration
let
R
be
rational-functions-valued
Relation
;
cluster
rng
R
->
rational-functions-membered
;
coherence
rng
R
is
rational-functions-membered
by
Def23
;
end;
registration
let
R
be
integer-functions-valued
Relation
;
cluster
rng
R
->
integer-functions-membered
;
coherence
rng
R
is
integer-functions-membered
by
Def24
;
end;
registration
let
R
be
natural-functions-valued
Relation
;
cluster
rng
R
->
natural-functions-membered
;
coherence
rng
R
is
natural-functions-membered
by
Def25
;
end;
registration
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
cluster
Function-like
->
complex-functions-valued
for
Element
of
K19
(
K20
(
X
,
Y
));
coherence
for
b
1
being
PartFunc
of
X
,
Y
holds
b
1
is
complex-functions-valued
;
end;
registration
let
X
be
set
;
let
Y
be
ext-real-functions-membered
set
;
cluster
Function-like
->
ext-real-functions-valued
for
Element
of
K19
(
K20
(
X
,
Y
));
coherence
for
b
1
being
PartFunc
of
X
,
Y
holds
b
1
is
ext-real-functions-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
cluster
Function-like
->
real-functions-valued
for
Element
of
K19
(
K20
(
X
,
Y
));
coherence
for
b
1
being
PartFunc
of
X
,
Y
holds
b
1
is
real-functions-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
cluster
Function-like
->
rational-functions-valued
for
Element
of
K19
(
K20
(
X
,
Y
));
coherence
for
b
1
being
PartFunc
of
X
,
Y
holds
b
1
is
rational-functions-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
integer-functions-membered
set
;
cluster
Function-like
->
integer-functions-valued
for
Element
of
K19
(
K20
(
X
,
Y
));
coherence
for
b
1
being
PartFunc
of
X
,
Y
holds
b
1
is
integer-functions-valued
proof
end;
end;
registration
let
X
be
set
;
let
Y
be
natural-functions-membered
set
;
cluster
Function-like
->
natural-functions-valued
for
Element
of
K19
(
K20
(
X
,
Y
));
coherence
for
b
1
being
PartFunc
of
X
,
Y
holds
b
1
is
natural-functions-valued
proof
end;
end;
registration
let
f
be
complex-functions-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
Relation-like
Function-like
;
coherence
(
f
.
x
is
Function-like
&
f
.
x
is
Relation-like
)
proof
end;
end;
registration
let
f
be
ext-real-functions-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
Relation-like
Function-like
;
coherence
(
f
.
x
is
Function-like
&
f
.
x
is
Relation-like
)
proof
end;
end;
registration
let
f
be
complex-functions-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
complex-valued
;
coherence
f
.
x
is
complex-valued
proof
end;
end;
registration
let
f
be
ext-real-functions-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
ext-real-valued
;
coherence
f
.
x
is
ext-real-valued
proof
end;
end;
registration
let
f
be
real-functions-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
real-valued
;
coherence
f
.
x
is
real-valued
proof
end;
end;
registration
let
f
be
rational-functions-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
RAT
-valued
;
coherence
f
.
x
is
RAT
-valued
proof
end;
end;
registration
let
f
be
integer-functions-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
INT
-valued
;
coherence
f
.
x
is
INT
-valued
proof
end;
end;
registration
let
f
be
natural-functions-valued
Function
;
let
x
be
set
;
cluster
f
.
x
->
natural-valued
;
coherence
f
.
x
is
natural-valued
proof
end;
end;
begin
theorem
Th7
:
:: VALUED_2:7
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
st
g
<>
{}
&
g
+
c1
=
g
+
c2
holds
c1
=
c2
proof
end;
theorem
Th8
:
:: VALUED_2:8
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
st
g
<>
{}
&
g
-
c1
=
g
-
c2
holds
c1
=
c2
proof
end;
theorem
Th9
:
:: VALUED_2:9
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
st
g
<>
{}
&
g
is
non-empty
&
g
(#)
c1
=
g
(#)
c2
holds
c1
=
c2
proof
end;
theorem
Th10
:
:: VALUED_2:10
for
c
being
complex
number
for
g
being
complex-valued
Function
holds
-
(
g
+
c
)
=
(
-
g
)
-
c
proof
end;
theorem
Th11
:
:: VALUED_2:11
for
c
being
complex
number
for
g
being
complex-valued
Function
holds
-
(
g
-
c
)
=
(
-
g
)
+
c
proof
end;
theorem
Th12
:
:: VALUED_2:12
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
holds
(
g
+
c1
)
+
c2
=
g
+
(
c1
+
c2
)
proof
end;
theorem
Th13
:
:: VALUED_2:13
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
holds
(
g
+
c1
)
-
c2
=
g
+
(
c1
-
c2
)
proof
end;
theorem
Th14
:
:: VALUED_2:14
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
holds
(
g
-
c1
)
+
c2
=
g
-
(
c1
-
c2
)
proof
end;
theorem
Th15
:
:: VALUED_2:15
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
holds
(
g
-
c1
)
-
c2
=
g
-
(
c1
+
c2
)
proof
end;
theorem
Th16
:
:: VALUED_2:16
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
holds
(
g
(#)
c1
)
(#)
c2
=
g
(#)
(
c1
*
c2
)
proof
end;
theorem
Th17
:
:: VALUED_2:17
for
g
,
h
being
complex-valued
Function
holds
-
(
g
+
h
)
=
(
-
g
)
-
h
proof
end;
theorem
Th18
:
:: VALUED_2:18
for
g
,
h
being
complex-valued
Function
holds
g
-
h
=
-
(
h
-
g
)
proof
end;
theorem
Th19
:
:: VALUED_2:19
for
g
,
h
,
k
being
complex-valued
Function
holds
(
g
(#)
h
)
/"
k
=
g
(#)
(
h
/"
k
)
proof
end;
theorem
Th20
:
:: VALUED_2:20
for
g
,
h
,
k
being
complex-valued
Function
holds
(
g
/"
h
)
(#)
k
=
(
g
(#)
k
)
/"
h
proof
end;
theorem
Th21
:
:: VALUED_2:21
for
g
,
h
,
k
being
complex-valued
Function
holds
(
g
/"
h
)
/"
k
=
g
/"
(
h
(#)
k
)
proof
end;
theorem
Th22
:
:: VALUED_2:22
for
c
being
complex
number
for
g
being
complex-valued
Function
holds
c
(#)
(
-
g
)
=
(
-
c
)
(#)
g
proof
end;
theorem
Th23
:
:: VALUED_2:23
for
c
being
complex
number
for
g
being
complex-valued
Function
holds
c
(#)
(
-
g
)
=
-
(
c
(#)
g
)
proof
end;
theorem
Th24
:
:: VALUED_2:24
for
c
being
complex
number
for
g
being
complex-valued
Function
holds
(
-
c
)
(#)
g
=
-
(
c
(#)
g
)
proof
end;
theorem
Th25
:
:: VALUED_2:25
for
g
,
h
being
complex-valued
Function
holds
-
(
g
(#)
h
)
=
(
-
g
)
(#)
h
proof
end;
theorem
:: VALUED_2:26
for
g
,
h
being
complex-valued
Function
holds
-
(
g
/"
h
)
=
(
-
g
)
/"
h
proof
end;
theorem
Th27
:
:: VALUED_2:27
for
g
,
h
being
complex-valued
Function
holds
-
(
g
/"
h
)
=
g
/"
(
-
h
)
proof
end;
definition
let
f
be
complex-valued
Function
;
let
c
be
complex
number
;
func
f
(/)
c
->
Function
equals
:: VALUED_2:def 32
(
1
/
c
)
(#)
f
;
coherence
(
1
/
c
)
(#)
f
is
Function
;
end;
::
deftheorem
defines
(/)
VALUED_2:def 32 :
for
f
being
complex-valued
Function
for
c
being
complex
number
holds
f
(/)
c
=
(
1
/
c
)
(#)
f
;
registration
let
f
be
complex-valued
Function
;
let
c
be
complex
number
;
cluster
f
(/)
c
->
complex-valued
;
coherence
f
(/)
c
is
complex-valued
;
end;
registration
let
f
be
real-valued
Function
;
let
r
be
real
number
;
cluster
f
(/)
r
->
real-valued
;
coherence
f
(/)
r
is
real-valued
;
end;
registration
let
f
be
RAT
-valued
Function
;
let
r
be
rational
number
;
cluster
f
(/)
r
->
RAT
-valued
;
coherence
f
(/)
r
is
RAT
-valued
;
end;
registration
let
f
be
complex-valued
FinSequence
;
let
c
be
complex
number
;
cluster
f
(/)
c
->
FinSequence-like
;
coherence
f
(/)
c
is
FinSequence-like
;
end;
theorem
:: VALUED_2:28
for
c
being
complex
number
for
g
being
complex-valued
Function
holds
dom
(
g
(/)
c
)
=
dom
g
by
VALUED_1:def 5
;
theorem
:: VALUED_2:29
for
x
being
set
for
c
being
complex
number
for
g
being
complex-valued
Function
holds
(
g
(/)
c
)
.
x
=
(
g
.
x
)
/
c
by
VALUED_1:6
;
theorem
Th30
:
:: VALUED_2:30
for
c
being
complex
number
for
g
being
complex-valued
Function
holds
(
-
g
)
(/)
c
=
-
(
g
(/)
c
)
proof
end;
theorem
Th31
:
:: VALUED_2:31
for
c
being
complex
number
for
g
being
complex-valued
Function
holds
g
(/)
(
-
c
)
=
-
(
g
(/)
c
)
proof
end;
theorem
:: VALUED_2:32
for
c
being
complex
number
for
g
being
complex-valued
Function
holds
g
(/)
(
-
c
)
=
(
-
g
)
(/)
c
proof
end;
theorem
Th33
:
:: VALUED_2:33
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
st
g
<>
{}
&
g
is
non-empty
&
g
(/)
c1
=
g
(/)
c2
holds
c1
=
c2
proof
end;
theorem
:: VALUED_2:34
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
holds
(
g
(#)
c1
)
(/)
c2
=
g
(#)
(
c1
/
c2
)
proof
end;
theorem
:: VALUED_2:35
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
holds
(
g
(/)
c1
)
(#)
c2
=
(
g
(#)
c2
)
(/)
c1
proof
end;
theorem
:: VALUED_2:36
for
c1
,
c2
being
complex
number
for
g
being
complex-valued
Function
holds
(
g
(/)
c1
)
(/)
c2
=
g
(/)
(
c1
*
c2
)
proof
end;
theorem
:: VALUED_2:37
for
c
being
complex
number
for
g
,
h
being
complex-valued
Function
holds
(
g
+
h
)
(/)
c
=
(
g
(/)
c
)
+
(
h
(/)
c
)
proof
end;
theorem
:: VALUED_2:38
for
c
being
complex
number
for
g
,
h
being
complex-valued
Function
holds
(
g
-
h
)
(/)
c
=
(
g
(/)
c
)
-
(
h
(/)
c
)
proof
end;
theorem
:: VALUED_2:39
for
c
being
complex
number
for
g
,
h
being
complex-valued
Function
holds
(
g
(#)
h
)
(/)
c
=
g
(#)
(
h
(/)
c
)
proof
end;
theorem
:: VALUED_2:40
for
c
being
complex
number
for
g
,
h
being
complex-valued
Function
holds
(
g
/"
h
)
(/)
c
=
g
/"
(
h
(#)
c
)
proof
end;
definition
let
f
be
complex-functions-valued
Function
;
deffunc
H
1
(
set
)
->
set
=
-
(
f
.
$1
)
;
func
<->
f
->
Function
means
:
Def33
:
:: VALUED_2:def 33
(
dom
it
=
dom
f
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
-
(
f
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
-
(
f
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
-
(
f
.
x
)
) &
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
-
(
f
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def33
defines
<->
VALUED_2:def 33 :
for
f
being
complex-functions-valued
Function
for
b
2
being
Function
holds
(
b
2
=
<->
f
iff (
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
-
(
f
.
x
)
) ) );
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
<->
redefine
func
<->
f
->
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
<->
f
is
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
<->
redefine
func
<->
f
->
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
<->
f
is
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
<->
redefine
func
<->
f
->
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
<->
f
is
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
<->
redefine
func
<->
f
->
PartFunc
of
X
,
(
I_PFuncs
(
DOMS
Y
)
)
;
coherence
<->
f
is
PartFunc
of
X
,
(
I_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
registration
let
Y
be
complex-functions-membered
set
;
let
f
be
FinSequence
of
Y
;
cluster
<->
f
->
FinSequence-like
;
coherence
<->
f
is
FinSequence-like
proof
end;
end;
theorem
:: VALUED_2:41
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
holds
<->
(
<->
f
)
=
f
proof
end;
theorem
:: VALUED_2:42
for
X1
,
X2
being
set
for
Y1
,
Y2
being
complex-functions-membered
set
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
st
<->
f1
=
<->
f2
holds
f1
=
f2
proof
end;
definition
let
X
be
complex-functions-membered
set
;
let
Y
be
set
;
let
f
be
PartFunc
of
X
,
Y
;
defpred
S
1
[
set
,
set
]
means
ex
a
being
complex-valued
Function
st
( $1
=
a
& $2
=
f
.
(
-
a
)
);
func
f
(-)
->
Function
means
:: VALUED_2:def 34
(
dom
it
=
dom
f
& ( for
x
being
complex-valued
Function
st
x
in
dom
it
holds
it
.
x
=
f
.
(
-
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
dom
f
& ( for
x
being
complex-valued
Function
st
x
in
dom
b
1
holds
b
1
.
x
=
f
.
(
-
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
dom
f
& ( for
x
being
complex-valued
Function
st
x
in
dom
b
1
holds
b
1
.
x
=
f
.
(
-
x
)
) &
dom
b
2
=
dom
f
& ( for
x
being
complex-valued
Function
st
x
in
dom
b
2
holds
b
2
.
x
=
f
.
(
-
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
defines
(-)
VALUED_2:def 34 :
for
X
being
complex-functions-membered
set
for
Y
being
set
for
f
being
PartFunc
of
X
,
Y
for
b
4
being
Function
holds
(
b
4
=
f
(-)
iff (
dom
b
4
=
dom
f
& ( for
x
being
complex-valued
Function
st
x
in
dom
b
4
holds
b
4
.
x
=
f
.
(
-
x
)
) ) );
definition
let
f
be
complex-functions-valued
Function
;
deffunc
H
1
(
set
)
->
set
=
(
f
.
$1
)
"
;
func
</>
f
->
Function
means
:
Def35
:
:: VALUED_2:def 35
(
dom
it
=
dom
f
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
(
f
.
x
)
"
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
"
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
"
) &
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
(
f
.
x
)
"
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def35
defines
</>
VALUED_2:def 35 :
for
f
being
complex-functions-valued
Function
for
b
2
being
Function
holds
(
b
2
=
</>
f
iff (
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
(
f
.
x
)
"
) ) );
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
</>
redefine
func
</>
f
->
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
</>
f
is
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
</>
redefine
func
</>
f
->
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
</>
f
is
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
</>
redefine
func
</>
f
->
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
</>
f
is
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
registration
let
Y
be
complex-functions-membered
set
;
let
f
be
FinSequence
of
Y
;
cluster
</>
f
->
FinSequence-like
;
coherence
</>
f
is
FinSequence-like
proof
end;
end;
theorem
:: VALUED_2:43
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
holds
</>
(
</>
f
)
=
f
proof
end;
definition
let
f
be
complex-functions-valued
Function
;
deffunc
H
1
(
set
)
->
set
=
abs
(
f
.
$1
)
;
func
abs
f
->
Function
means
:
Def36
:
:: VALUED_2:def 36
(
dom
it
=
dom
f
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
abs
(
f
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
abs
(
f
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
abs
(
f
.
x
)
) &
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
abs
(
f
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def36
defines
abs
VALUED_2:def 36 :
for
f
being
complex-functions-valued
Function
for
b
2
being
Function
holds
(
b
2
=
abs
f
iff (
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
abs
(
f
.
x
)
) ) );
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
abs
redefine
func
abs
f
->
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
abs
f
is
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
abs
redefine
func
abs
f
->
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
abs
f
is
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
abs
redefine
func
abs
f
->
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
abs
f
is
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
:: original:
abs
redefine
func
abs
f
->
PartFunc
of
X
,
(
N_PFuncs
(
DOMS
Y
)
)
;
coherence
abs
f
is
PartFunc
of
X
,
(
N_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
registration
let
Y
be
complex-functions-membered
set
;
let
f
be
FinSequence
of
Y
;
cluster
abs
f
->
FinSequence-like
;
coherence
abs
f
is
FinSequence-like
proof
end;
end;
theorem
:: VALUED_2:44
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
holds
abs
(
abs
f
)
=
abs
f
proof
end;
definition
let
Y
be
complex-functions-membered
set
;
let
f
be
Y
-valued
Function
;
let
c
be
complex
number
;
deffunc
H
1
(
set
)
->
set
=
c
+
(
f
.
$1
)
;
func
f
[+]
c
->
Function
means
:
Def37
:
:: VALUED_2:def 37
(
dom
it
=
dom
f
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
c
+
(
f
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
c
+
(
f
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
c
+
(
f
.
x
)
) &
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
c
+
(
f
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def37
defines
[+]
VALUED_2:def 37 :
for
Y
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
c
being
complex
number
for
b
4
being
Function
holds
(
b
4
=
f
[+]
c
iff (
dom
b
4
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
4
holds
b
4
.
x
=
c
+
(
f
.
x
)
) ) );
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
complex
number
;
:: original:
[+]
redefine
func
f
[+]
c
->
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[+]
c
is
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
real
number
;
:: original:
[+]
redefine
func
f
[+]
c
->
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[+]
c
is
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
rational
number
;
:: original:
[+]
redefine
func
f
[+]
c
->
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[+]
c
is
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
integer
number
;
:: original:
[+]
redefine
func
f
[+]
c
->
PartFunc
of
X
,
(
I_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[+]
c
is
PartFunc
of
X
,
(
I_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
natural-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
Nat
;
:: original:
[+]
redefine
func
f
[+]
c
->
PartFunc
of
X
,
(
N_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[+]
c
is
PartFunc
of
X
,
(
N_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
theorem
:: VALUED_2:45
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c1
,
c2
being
complex
number
for
f
being
PartFunc
of
X
,
Y
holds
(
f
[+]
c1
)
[+]
c2
=
f
[+]
(
c1
+
c2
)
proof
end;
theorem
:: VALUED_2:46
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c1
,
c2
being
complex
number
for
f
being
PartFunc
of
X
,
Y
st
f
<>
{}
&
f
is
non-empty
&
f
[+]
c1
=
f
[+]
c2
holds
c1
=
c2
proof
end;
definition
let
Y
be
complex-functions-membered
set
;
let
f
be
Y
-valued
Function
;
let
c
be
complex
number
;
func
f
[-]
c
->
Function
equals
:: VALUED_2:def 38
f
[+]
(
-
c
)
;
coherence
f
[+]
(
-
c
)
is
Function
;
end;
::
deftheorem
defines
[-]
VALUED_2:def 38 :
for
Y
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
c
being
complex
number
holds
f
[-]
c
=
f
[+]
(
-
c
)
;
theorem
:: VALUED_2:47
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c
being
complex
number
for
f
being
PartFunc
of
X
,
Y
holds
dom
(
f
[-]
c
)
=
dom
f
by
Def37
;
theorem
:: VALUED_2:48
for
X
,
x
being
set
for
Y
being
complex-functions-membered
set
for
c
being
complex
number
for
f
being
PartFunc
of
X
,
Y
st
x
in
dom
(
f
[-]
c
)
holds
(
f
[-]
c
)
.
x
=
(
f
.
x
)
-
c
by
Def37
;
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
complex
number
;
:: original:
[-]
redefine
func
f
[-]
c
->
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[-]
c
is
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
real
number
;
:: original:
[-]
redefine
func
f
[-]
c
->
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[-]
c
is
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
rational
number
;
:: original:
[-]
redefine
func
f
[-]
c
->
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[-]
c
is
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
integer
number
;
:: original:
[-]
redefine
func
f
[-]
c
->
PartFunc
of
X
,
(
I_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[-]
c
is
PartFunc
of
X
,
(
I_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
theorem
:: VALUED_2:49
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c1
,
c2
being
complex
number
for
f
being
PartFunc
of
X
,
Y
st
f
<>
{}
&
f
is
non-empty
&
f
[-]
c1
=
f
[-]
c2
holds
c1
=
c2
proof
end;
theorem
:: VALUED_2:50
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c1
,
c2
being
complex
number
for
f
being
PartFunc
of
X
,
Y
holds
(
f
[+]
c1
)
[-]
c2
=
f
[+]
(
c1
-
c2
)
proof
end;
theorem
:: VALUED_2:51
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c1
,
c2
being
complex
number
for
f
being
PartFunc
of
X
,
Y
holds
(
f
[-]
c1
)
[+]
c2
=
f
[-]
(
c1
-
c2
)
proof
end;
theorem
:: VALUED_2:52
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c1
,
c2
being
complex
number
for
f
being
PartFunc
of
X
,
Y
holds
(
f
[-]
c1
)
[-]
c2
=
f
[-]
(
c1
+
c2
)
proof
end;
definition
let
Y
be
complex-functions-membered
set
;
let
f
be
Y
-valued
Function
;
let
c
be
complex
number
;
deffunc
H
1
(
set
)
->
set
=
c
(#)
(
f
.
$1
)
;
func
f
[#]
c
->
Function
means
:
Def39
:
:: VALUED_2:def 39
(
dom
it
=
dom
f
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
c
(#)
(
f
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
c
(#)
(
f
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
c
(#)
(
f
.
x
)
) &
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
c
(#)
(
f
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def39
defines
[#]
VALUED_2:def 39 :
for
Y
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
c
being
complex
number
for
b
4
being
Function
holds
(
b
4
=
f
[#]
c
iff (
dom
b
4
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
4
holds
b
4
.
x
=
c
(#)
(
f
.
x
)
) ) );
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
complex
number
;
:: original:
[#]
redefine
func
f
[#]
c
->
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[#]
c
is
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
real
number
;
:: original:
[#]
redefine
func
f
[#]
c
->
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[#]
c
is
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
rational
number
;
:: original:
[#]
redefine
func
f
[#]
c
->
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[#]
c
is
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
integer
number
;
:: original:
[#]
redefine
func
f
[#]
c
->
PartFunc
of
X
,
(
I_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[#]
c
is
PartFunc
of
X
,
(
I_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
natural-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
Nat
;
:: original:
[#]
redefine
func
f
[#]
c
->
PartFunc
of
X
,
(
N_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[#]
c
is
PartFunc
of
X
,
(
N_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
theorem
:: VALUED_2:53
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c1
,
c2
being
complex
number
for
f
being
PartFunc
of
X
,
Y
holds
(
f
[#]
c1
)
[#]
c2
=
f
[#]
(
c1
*
c2
)
proof
end;
theorem
:: VALUED_2:54
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c1
,
c2
being
complex
number
for
f
being
PartFunc
of
X
,
Y
st
f
<>
{}
&
f
is
non-empty
& ( for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
non-empty
) &
f
[#]
c1
=
f
[#]
c2
holds
c1
=
c2
proof
end;
definition
let
Y
be
complex-functions-membered
set
;
let
f
be
Y
-valued
Function
;
let
c
be
complex
number
;
func
f
[/]
c
->
Function
equals
:: VALUED_2:def 40
f
[#]
(
c
"
)
;
coherence
f
[#]
(
c
"
)
is
Function
;
end;
::
deftheorem
defines
[/]
VALUED_2:def 40 :
for
Y
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
c
being
complex
number
holds
f
[/]
c
=
f
[#]
(
c
"
)
;
theorem
:: VALUED_2:55
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c
being
complex
number
for
f
being
PartFunc
of
X
,
Y
holds
dom
(
f
[/]
c
)
=
dom
f
by
Def39
;
theorem
:: VALUED_2:56
for
X
,
x
being
set
for
Y
being
complex-functions-membered
set
for
c
being
complex
number
for
f
being
PartFunc
of
X
,
Y
st
x
in
dom
(
f
[/]
c
)
holds
(
f
[/]
c
)
.
x
=
(
c
"
)
(#)
(
f
.
x
)
by
Def39
;
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
complex
number
;
:: original:
[/]
redefine
func
f
[/]
c
->
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[/]
c
is
PartFunc
of
X
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
real
number
;
:: original:
[/]
redefine
func
f
[/]
c
->
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[/]
c
is
PartFunc
of
X
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
c
be
rational
number
;
:: original:
[/]
redefine
func
f
[/]
c
->
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
f
[/]
c
is
PartFunc
of
X
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
theorem
:: VALUED_2:57
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c1
,
c2
being
complex
number
for
f
being
PartFunc
of
X
,
Y
holds
(
f
[/]
c1
)
[/]
c2
=
f
[/]
(
c1
*
c2
)
proof
end;
theorem
:: VALUED_2:58
for
X
being
set
for
Y
being
complex-functions-membered
set
for
c1
,
c2
being
complex
number
for
f
being
PartFunc
of
X
,
Y
st
f
<>
{}
&
f
is
non-empty
& ( for
x
being
set
st
x
in
dom
f
holds
f
.
x
is
non-empty
) &
f
[/]
c1
=
f
[/]
c2
holds
c1
=
c2
proof
end;
definition
let
Y
be
complex-functions-membered
set
;
let
f
be
Y
-valued
Function
;
let
g
be
complex-valued
Function
;
deffunc
H
1
(
set
)
->
set
=
(
f
.
$1
)
+
(
g
.
$1
)
;
func
f
<+>
g
->
Function
means
:
Def41
:
:: VALUED_2:def 41
(
dom
it
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
(
f
.
x
)
+
(
g
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
+
(
g
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
+
(
g
.
x
)
) &
dom
b
2
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
(
f
.
x
)
+
(
g
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def41
defines
<+>
VALUED_2:def 41 :
for
Y
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
g
being
complex-valued
Function
for
b
4
being
Function
holds
(
b
4
=
f
<+>
g
iff (
dom
b
4
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
4
holds
b
4
.
x
=
(
f
.
x
)
+
(
g
.
x
)
) ) );
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
complex-valued
Function
;
:: original:
<+>
redefine
func
f
<+>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<+>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
real-valued
Function
;
:: original:
<+>
redefine
func
f
<+>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<+>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
RAT
-valued
Function
;
:: original:
<+>
redefine
func
f
<+>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<+>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
INT
-valued
Function
;
:: original:
<+>
redefine
func
f
<+>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
I_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<+>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
I_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
natural-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
natural-valued
Function
;
:: original:
<+>
redefine
func
f
<+>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
N_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<+>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
N_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
theorem
:: VALUED_2:59
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
,
h
being
complex-valued
Function
holds
(
f
<+>
g
)
<+>
h
=
f
<+>
(
g
+
h
)
proof
end;
theorem
:: VALUED_2:60
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
being
complex-valued
Function
holds
<->
(
f
<+>
g
)
=
(
<->
f
)
<+>
(
-
g
)
proof
end;
definition
let
Y
be
complex-functions-membered
set
;
let
f
be
Y
-valued
Function
;
let
g
be
complex-valued
Function
;
func
f
<->
g
->
Function
equals
:: VALUED_2:def 42
f
<+>
(
-
g
)
;
coherence
f
<+>
(
-
g
)
is
Function
;
end;
::
deftheorem
defines
<->
VALUED_2:def 42 :
for
Y
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
g
being
complex-valued
Function
holds
f
<->
g
=
f
<+>
(
-
g
)
;
theorem
Th61
:
:: VALUED_2:61
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
being
complex-valued
Function
holds
dom
(
f
<->
g
)
=
(
dom
f
)
/\
(
dom
g
)
proof
end;
theorem
Th62
:
:: VALUED_2:62
for
X
,
x
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
being
complex-valued
Function
st
x
in
dom
(
f
<->
g
)
holds
(
f
<->
g
)
.
x
=
(
f
.
x
)
-
(
g
.
x
)
proof
end;
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
complex-valued
Function
;
:: original:
<->
redefine
func
f
<->
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<->
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
real-valued
Function
;
:: original:
<->
redefine
func
f
<->
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<->
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
RAT
-valued
Function
;
:: original:
<->
redefine
func
f
<->
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<->
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
INT
-valued
Function
;
:: original:
<->
redefine
func
f
<->
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
I_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<->
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
I_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
theorem
:: VALUED_2:63
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
being
complex-valued
Function
holds
f
<->
(
-
g
)
=
f
<+>
g
;
theorem
:: VALUED_2:64
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
being
complex-valued
Function
holds
<->
(
f
<->
g
)
=
(
<->
f
)
<+>
g
proof
end;
theorem
:: VALUED_2:65
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
,
h
being
complex-valued
Function
holds
(
f
<+>
g
)
<->
h
=
f
<+>
(
g
-
h
)
proof
end;
theorem
:: VALUED_2:66
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
,
h
being
complex-valued
Function
holds
(
f
<->
g
)
<+>
h
=
f
<->
(
g
-
h
)
proof
end;
theorem
:: VALUED_2:67
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
,
h
being
complex-valued
Function
holds
(
f
<->
g
)
<->
h
=
f
<->
(
g
+
h
)
proof
end;
definition
let
Y
be
complex-functions-membered
set
;
let
f
be
Y
-valued
Function
;
let
g
be
complex-valued
Function
;
deffunc
H
1
(
set
)
->
set
=
(
f
.
$1
)
(#)
(
g
.
$1
)
;
func
f
<#>
g
->
Function
means
:
Def43
:
:: VALUED_2:def 43
(
dom
it
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
(
f
.
x
)
(#)
(
g
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
(#)
(
g
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
(#)
(
g
.
x
)
) &
dom
b
2
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
(
f
.
x
)
(#)
(
g
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def43
defines
<#>
VALUED_2:def 43 :
for
Y
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
g
being
complex-valued
Function
for
b
4
being
Function
holds
(
b
4
=
f
<#>
g
iff (
dom
b
4
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
4
holds
b
4
.
x
=
(
f
.
x
)
(#)
(
g
.
x
)
) ) );
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
complex-valued
Function
;
:: original:
<#>
redefine
func
f
<#>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<#>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
real-valued
Function
;
:: original:
<#>
redefine
func
f
<#>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<#>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
RAT
-valued
Function
;
:: original:
<#>
redefine
func
f
<#>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<#>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
INT
-valued
Function
;
:: original:
<#>
redefine
func
f
<#>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
I_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<#>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
I_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
natural-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
natural-valued
Function
;
:: original:
<#>
redefine
func
f
<#>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
N_PFuncs
(
DOMS
Y
)
)
;
coherence
f
<#>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
N_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
theorem
:: VALUED_2:68
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
being
complex-valued
Function
holds
f
<#>
(
-
g
)
=
(
<->
f
)
<#>
g
proof
end;
theorem
:: VALUED_2:69
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
being
complex-valued
Function
holds
f
<#>
(
-
g
)
=
<->
(
f
<#>
g
)
proof
end;
theorem
:: VALUED_2:70
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
,
h
being
complex-valued
Function
holds
(
f
<#>
g
)
<#>
h
=
f
<#>
(
g
(#)
h
)
proof
end;
definition
let
Y
be
complex-functions-membered
set
;
let
f
be
Y
-valued
Function
;
let
g
be
complex-valued
Function
;
func
f
</>
g
->
Function
equals
:: VALUED_2:def 44
f
<#>
(
g
"
)
;
coherence
f
<#>
(
g
"
)
is
Function
;
end;
::
deftheorem
defines
</>
VALUED_2:def 44 :
for
Y
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
g
being
complex-valued
Function
holds
f
</>
g
=
f
<#>
(
g
"
)
;
theorem
Th71
:
:: VALUED_2:71
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
being
complex-valued
Function
holds
dom
(
f
</>
g
)
=
(
dom
f
)
/\
(
dom
g
)
proof
end;
theorem
Th72
:
:: VALUED_2:72
for
X
,
x
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
being
complex-valued
Function
st
x
in
dom
(
f
</>
g
)
holds
(
f
</>
g
)
.
x
=
(
f
.
x
)
(/)
(
g
.
x
)
proof
end;
definition
let
X
be
set
;
let
Y
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
complex-valued
Function
;
:: original:
</>
redefine
func
f
</>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
C_PFuncs
(
DOMS
Y
)
)
;
coherence
f
</>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
C_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
real-valued
Function
;
:: original:
</>
redefine
func
f
</>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
R_PFuncs
(
DOMS
Y
)
)
;
coherence
f
</>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
R_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
definition
let
X
be
set
;
let
Y
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X
,
Y
;
let
g
be
RAT
-valued
Function
;
:: original:
</>
redefine
func
f
</>
g
->
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
Q_PFuncs
(
DOMS
Y
)
)
;
coherence
f
</>
g
is
PartFunc
of
(
X
/\
(
dom
g
)
)
,
(
Q_PFuncs
(
DOMS
Y
)
)
proof
end;
end;
theorem
:: VALUED_2:73
for
X
being
set
for
Y
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
g
,
h
being
complex-valued
Function
holds
(
f
<#>
g
)
</>
h
=
f
<#>
(
g
/"
h
)
proof
end;
definition
let
Y1
,
Y2
be
complex-functions-membered
set
;
let
f
be
Y1
-valued
Function
;
let
g
be
Y2
-valued
Function
;
deffunc
H
1
(
set
)
->
set
=
(
f
.
$1
)
+
(
g
.
$1
)
;
func
f
<++>
g
->
Function
means
:
Def45
:
:: VALUED_2:def 45
(
dom
it
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
(
f
.
x
)
+
(
g
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
+
(
g
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
+
(
g
.
x
)
) &
dom
b
2
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
(
f
.
x
)
+
(
g
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def45
defines
<++>
VALUED_2:def 45 :
for
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
g
being
b
2
-valued
Function
for
b
5
being
Function
holds
(
b
5
=
f
<++>
g
iff (
dom
b
5
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
5
holds
b
5
.
x
=
(
f
.
x
)
+
(
g
.
x
)
) ) );
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<++>
redefine
func
f
<++>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
C_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<++>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
C_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<++>
redefine
func
f
<++>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
R_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<++>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
R_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<++>
redefine
func
f
<++>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
Q_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<++>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
Q_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<++>
redefine
func
f
<++>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
I_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<++>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
I_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
natural-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<++>
redefine
func
f
<++>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
N_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<++>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
N_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
theorem
:: VALUED_2:74
for
X1
,
X2
being
set
for
Y1
,
Y2
being
complex-functions-membered
set
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
f1
<++>
f2
=
f2
<++>
f1
proof
end;
theorem
:: VALUED_2:75
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f
<++>
f1
)
<++>
f2
=
f
<++>
(
f1
<++>
f2
)
proof
end;
theorem
:: VALUED_2:76
for
X1
,
X2
being
set
for
Y1
,
Y2
being
complex-functions-membered
set
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
<->
(
f1
<++>
f2
)
=
(
<->
f1
)
<++>
(
<->
f2
)
proof
end;
definition
let
Y1
,
Y2
be
complex-functions-membered
set
;
let
f
be
Y1
-valued
Function
;
let
g
be
Y2
-valued
Function
;
deffunc
H
1
(
set
)
->
set
=
(
f
.
$1
)
-
(
g
.
$1
)
;
func
f
<-->
g
->
Function
means
:
Def46
:
:: VALUED_2:def 46
(
dom
it
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
(
f
.
x
)
-
(
g
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
-
(
g
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
-
(
g
.
x
)
) &
dom
b
2
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
(
f
.
x
)
-
(
g
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def46
defines
<-->
VALUED_2:def 46 :
for
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
g
being
b
2
-valued
Function
for
b
5
being
Function
holds
(
b
5
=
f
<-->
g
iff (
dom
b
5
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
5
holds
b
5
.
x
=
(
f
.
x
)
-
(
g
.
x
)
) ) );
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<-->
redefine
func
f
<-->
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
C_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<-->
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
C_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<-->
redefine
func
f
<-->
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
R_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<-->
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
R_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<-->
redefine
func
f
<-->
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
Q_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<-->
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
Q_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<-->
redefine
func
f
<-->
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
I_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<-->
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
I_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
theorem
:: VALUED_2:77
for
X1
,
X2
being
set
for
Y1
,
Y2
being
complex-functions-membered
set
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
f1
<-->
f2
=
<->
(
f2
<-->
f1
)
proof
end;
theorem
:: VALUED_2:78
for
X1
,
X2
being
set
for
Y1
,
Y2
being
complex-functions-membered
set
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
<->
(
f1
<-->
f2
)
=
(
<->
f1
)
<++>
f2
proof
end;
theorem
:: VALUED_2:79
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f
<++>
f1
)
<-->
f2
=
f
<++>
(
f1
<-->
f2
)
proof
end;
theorem
:: VALUED_2:80
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f
<-->
f1
)
<++>
f2
=
f
<-->
(
f1
<-->
f2
)
proof
end;
theorem
:: VALUED_2:81
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f
<-->
f1
)
<-->
f2
=
f
<-->
(
f1
<++>
f2
)
proof
end;
theorem
:: VALUED_2:82
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f
<-->
f1
)
<-->
f2
=
(
f
<-->
f2
)
<-->
f1
proof
end;
definition
let
Y1
,
Y2
be
complex-functions-membered
set
;
let
f
be
Y1
-valued
Function
;
let
g
be
Y2
-valued
Function
;
deffunc
H
1
(
set
)
->
set
=
(
f
.
$1
)
(#)
(
g
.
$1
)
;
func
f
<##>
g
->
Function
means
:
Def47
:
:: VALUED_2:def 47
(
dom
it
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
(
f
.
x
)
(#)
(
g
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
(#)
(
g
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
(#)
(
g
.
x
)
) &
dom
b
2
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
(
f
.
x
)
(#)
(
g
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def47
defines
<##>
VALUED_2:def 47 :
for
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
g
being
b
2
-valued
Function
for
b
5
being
Function
holds
(
b
5
=
f
<##>
g
iff (
dom
b
5
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
5
holds
b
5
.
x
=
(
f
.
x
)
(#)
(
g
.
x
)
) ) );
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<##>
redefine
func
f
<##>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
C_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<##>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
C_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<##>
redefine
func
f
<##>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
R_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<##>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
R_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<##>
redefine
func
f
<##>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
Q_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<##>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
Q_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
integer-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<##>
redefine
func
f
<##>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
I_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<##>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
I_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
natural-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<##>
redefine
func
f
<##>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
N_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<##>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
N_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
theorem
Th83
:
:: VALUED_2:83
for
X1
,
X2
being
set
for
Y1
,
Y2
being
complex-functions-membered
set
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
f1
<##>
f2
=
f2
<##>
f1
proof
end;
theorem
:: VALUED_2:84
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f
<##>
f1
)
<##>
f2
=
f
<##>
(
f1
<##>
f2
)
proof
end;
theorem
:: VALUED_2:85
for
X1
,
X2
being
set
for
Y1
,
Y2
being
complex-functions-membered
set
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
<->
f1
)
<##>
f2
=
<->
(
f1
<##>
f2
)
proof
end;
theorem
:: VALUED_2:86
for
X1
,
X2
being
set
for
Y1
,
Y2
being
complex-functions-membered
set
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
f1
<##>
(
<->
f2
)
=
<->
(
f1
<##>
f2
)
proof
end;
theorem
Th87
:
:: VALUED_2:87
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
f
<##>
(
f1
<++>
f2
)
=
(
f
<##>
f1
)
<++>
(
f
<##>
f2
)
proof
end;
theorem
:: VALUED_2:88
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f1
<++>
f2
)
<##>
f
=
(
f1
<##>
f
)
<++>
(
f2
<##>
f
)
proof
end;
theorem
Th89
:
:: VALUED_2:89
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
f
<##>
(
f1
<-->
f2
)
=
(
f
<##>
f1
)
<-->
(
f
<##>
f2
)
proof
end;
theorem
:: VALUED_2:90
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f1
<-->
f2
)
<##>
f
=
(
f1
<##>
f
)
<-->
(
f2
<##>
f
)
proof
end;
definition
let
Y1
,
Y2
be
complex-functions-membered
set
;
let
f
be
Y1
-valued
Function
;
let
g
be
Y2
-valued
Function
;
deffunc
H
1
(
set
)
->
set
=
(
f
.
$1
)
/"
(
g
.
$1
)
;
func
f
<//>
g
->
Function
means
:
Def48
:
:: VALUED_2:def 48
(
dom
it
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
(
f
.
x
)
/"
(
g
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
/"
(
g
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
(
f
.
x
)
/"
(
g
.
x
)
) &
dom
b
2
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
(
f
.
x
)
/"
(
g
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def48
defines
<//>
VALUED_2:def 48 :
for
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
b
1
-valued
Function
for
g
being
b
2
-valued
Function
for
b
5
being
Function
holds
(
b
5
=
f
<//>
g
iff (
dom
b
5
=
(
dom
f
)
/\
(
dom
g
)
& ( for
x
being
set
st
x
in
dom
b
5
holds
b
5
.
x
=
(
f
.
x
)
/"
(
g
.
x
)
) ) );
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
complex-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<//>
redefine
func
f
<//>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
C_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<//>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
C_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
real-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<//>
redefine
func
f
<//>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
R_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<//>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
R_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
definition
let
X1
,
X2
be
set
;
let
Y1
,
Y2
be
rational-functions-membered
set
;
let
f
be
PartFunc
of
X1
,
Y1
;
let
g
be
PartFunc
of
X2
,
Y2
;
:: original:
<//>
redefine
func
f
<//>
g
->
PartFunc
of
(
X1
/\
X2
)
,
(
Q_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
;
coherence
f
<//>
g
is
PartFunc
of
(
X1
/\
X2
)
,
(
Q_PFuncs
(
(
DOMS
Y1
)
/\
(
DOMS
Y2
)
)
)
proof
end;
end;
theorem
:: VALUED_2:91
for
X1
,
X2
being
set
for
Y1
,
Y2
being
complex-functions-membered
set
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
<->
f1
)
<//>
f2
=
<->
(
f1
<//>
f2
)
proof
end;
theorem
:: VALUED_2:92
for
X1
,
X2
being
set
for
Y1
,
Y2
being
complex-functions-membered
set
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
f1
<//>
(
<->
f2
)
=
<->
(
f1
<//>
f2
)
proof
end;
theorem
:: VALUED_2:93
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f
<##>
f1
)
<//>
f2
=
f
<##>
(
f1
<//>
f2
)
proof
end;
theorem
:: VALUED_2:94
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f
<//>
f1
)
<##>
f2
=
(
f
<##>
f2
)
<//>
f1
proof
end;
theorem
:: VALUED_2:95
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f
<//>
f1
)
<//>
f2
=
f
<//>
(
f1
<##>
f2
)
proof
end;
theorem
:: VALUED_2:96
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f1
<++>
f2
)
<//>
f
=
(
f1
<//>
f
)
<++>
(
f2
<//>
f
)
proof
end;
theorem
:: VALUED_2:97
for
X
,
X1
,
X2
being
set
for
Y
,
Y1
,
Y2
being
complex-functions-membered
set
for
f
being
PartFunc
of
X
,
Y
for
f1
being
PartFunc
of
X1
,
Y1
for
f2
being
PartFunc
of
X2
,
Y2
holds
(
f1
<-->
f2
)
<//>
f
=
(
f1
<//>
f
)
<-->
(
f2
<//>
f
)
proof
end;