:: GRFUNC_1 semantic presentation
begin
theorem
:: GRFUNC_1:1
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
for
G
being ( ( ) ( )
set
) st
G
: ( ( ) ( )
set
)
c=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
G
: ( ( ) ( )
set
) is ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
theorem
:: GRFUNC_1:2
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) iff (
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
)
c=
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) & ( for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: GRFUNC_1:3
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
)
=
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
theorem
:: GRFUNC_1:4
for
x
,
z
being ( ( ) ( )
set
)
for
g
,
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
[
x
: ( ( ) ( )
set
) ,
z
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
in
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
*
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
) holds
(
[
x
: ( ( ) ( )
set
) ,
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
in
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) &
[
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
) ,
z
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
in
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ) ;
theorem
:: GRFUNC_1:5
for
x
,
y
being ( ( ) ( )
set
) holds
{
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
}
: ( ( ) (
Relation-like
Function-like
)
set
) is ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
theorem
:: GRFUNC_1:6
for
x
,
y
being ( ( ) ( )
set
)
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
=
{
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
}
: ( ( ) (
Relation-like
Function-like
)
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
y
: ( ( ) ( )
set
) ;
theorem
:: GRFUNC_1:7
for
x
being ( ( ) ( )
set
)
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
)
=
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( )
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
=
{
[
x
: ( ( ) ( )
set
) ,
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
}
: ( ( ) (
Relation-like
Function-like
)
set
) ;
theorem
:: GRFUNC_1:8
for
x1
,
y1
,
x2
,
y2
being ( ( ) ( )
set
) holds
(
{
[
x1
: ( ( ) ( )
set
) ,
y1
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
) ,
[
x2
: ( ( ) ( )
set
) ,
y2
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
}
: ( ( ) (
Relation-like
)
set
) is ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) iff (
x1
: ( ( ) ( )
set
)
=
x2
: ( ( ) ( )
set
) implies
y1
: ( ( ) ( )
set
)
=
y2
: ( ( ) ( )
set
) ) ) ;
theorem
:: GRFUNC_1:9
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
iff for
x1
,
x2
,
y
being ( ( ) ( )
set
) st
[
x1
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
in
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) &
[
x2
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
in
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
x1
: ( ( ) ( )
set
)
=
x2
: ( ( ) ( )
set
) ) ;
theorem
:: GRFUNC_1:10
for
g
,
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
holds
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
;
registration
let
f
be ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
let
X
be ( ( ) ( )
set
) ;
cluster
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
/\
X
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
)
set
)
->
Function-like
;
end;
theorem
:: GRFUNC_1:11
for
x
being ( ( ) ( )
set
)
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
x
: ( ( ) ( )
set
)
in
dom
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
/\
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) (
Relation-like
Function-like
)
set
) : ( ( ) ( )
set
) holds
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
/\
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) (
Relation-like
Function-like
)
set
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
theorem
:: GRFUNC_1:12
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
/\
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) (
Relation-like
Function-like
)
set
) is
one-to-one
;
theorem
:: GRFUNC_1:13
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
)
misses
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
\/
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) (
Relation-like
)
set
) is ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
theorem
:: GRFUNC_1:14
for
f
,
h
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) &
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
\/
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) (
Relation-like
)
set
) is ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
theorem
:: GRFUNC_1:15
for
x
being ( ( ) ( )
set
)
for
g
,
h
,
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
x
: ( ( ) ( )
set
)
in
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
\/
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) (
Relation-like
)
set
) holds
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
theorem
:: GRFUNC_1:16
for
x
being ( ( ) ( )
set
)
for
h
,
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
x
: ( ( ) ( )
set
)
in
dom
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
\/
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) (
Relation-like
)
set
) & not
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
) holds
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
theorem
:: GRFUNC_1:17
for
f
,
g
,
h
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
&
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
&
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
\/
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) (
Relation-like
)
set
) &
rng
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
)
misses
rng
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) holds
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
;
theorem
:: GRFUNC_1:18
canceled;
theorem
:: GRFUNC_1:19
canceled;
theorem
:: GRFUNC_1:20
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
holds
for
x
,
y
being ( ( ) ( )
set
) holds
(
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
in
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
"
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
) iff
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
in
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ) ;
theorem
:: GRFUNC_1:21
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
=
{}
: ( ( ) ( )
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
"
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
=
{}
: ( ( ) ( )
set
) ;
theorem
:: GRFUNC_1:22
for
x
,
X
being ( ( ) ( )
set
)
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
( (
x
: ( ( ) ( )
set
)
in
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) ) iff
[
x
: ( ( ) ( )
set
) ,
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
in
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
X
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
) ) ;
theorem
:: GRFUNC_1:23
for
g
,
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
(
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
theorem
:: GRFUNC_1:24
for
x
,
Y
being ( ( ) ( )
set
)
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
( (
x
: ( ( ) ( )
set
)
in
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
in
Y
: ( ( ) ( )
set
) ) iff
[
x
: ( ( ) ( )
set
) ,
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
in
Y
: ( ( ) ( )
set
)
|`
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
) ) ;
theorem
:: GRFUNC_1:25
for
g
,
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
holds
(
rng
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
)
|`
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
theorem
:: GRFUNC_1:26
for
x
,
Y
being ( ( ) ( )
set
)
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
(
x
: ( ( ) ( )
set
)
in
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
"
Y
: ( ( ) ( )
set
) : ( ( ) ( )
set
) iff (
[
x
: ( ( ) ( )
set
) ,
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
in
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
in
Y
: ( ( ) ( )
set
) ) ) ;
begin
theorem
:: GRFUNC_1:27
for
X
being ( ( ) ( )
set
)
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
X
: ( ( ) ( )
set
)
c=
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
X
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
X
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
) ;
theorem
:: GRFUNC_1:28
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
)
=
{
[
x
: ( ( ) ( )
set
) ,
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
)
]
: ( ( ) (
V14
() )
set
)
}
: ( ( ) (
Relation-like
Function-like
)
set
) ;
theorem
:: GRFUNC_1:29
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
for
x
being ( ( ) ( )
set
) st
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
)
=
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
) ;
theorem
:: GRFUNC_1:30
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
for
x
,
y
being ( ( ) ( )
set
) st
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
)
=
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
y
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
y
: ( ( ) ( )
set
) : ( ( ) ( )
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
{
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
}
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
{
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
}
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
) ;
theorem
:: GRFUNC_1:31
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
for
x
,
y
,
z
being ( ( ) ( )
set
) st
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
)
=
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
y
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
y
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
z
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
z
: ( ( ) ( )
set
) : ( ( ) ( )
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
{
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
) ,
z
: ( ( ) ( )
set
)
}
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
{
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
) ,
z
: ( ( ) ( )
set
)
}
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
) ;
registration
let
f
be ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
let
A
be ( ( ) ( )
set
) ;
cluster
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
\
A
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
)
set
)
->
Function-like
;
end;
theorem
:: GRFUNC_1:32
for
x
being ( ( ) ( )
set
)
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
x
: ( ( ) ( )
set
)
in
(
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
)
\
(
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of
K10
(
(
dom
b
2
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) holds
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
\
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) (
Relation-like
Function-like
)
Element
of
K10
(
b
2
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ) : ( ( ) ( )
set
) )
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
theorem
:: GRFUNC_1:33
for
f
,
g
,
h
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
(
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
)
=
h
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
(
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
) ;
registration
let
f
be ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
let
g
be ( ( ) (
Relation-like
Function-like
)
Subset
of ( ( ) ( )
set
) ) ;
cluster
Relation-like
Function-like
g
: ( ( ) ( )
set
)
-compatible
->
Relation-like
Function-like
f
: ( ( ) ( )
set
)
-compatible
for ( ( ) ( )
set
) ;
end;
theorem
:: GRFUNC_1:34
for
g
,
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) holds
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
|
(
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
) ;
registration
let
f
be ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
let
g
be ( (
Relation-like
Function-like
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
-compatible
) (
Relation-like
Function-like
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
-compatible
)
Function
) ;
cluster
->
f
: ( ( ) ( )
set
)
-compatible
for ( ( ) ( )
Element
of
K10
(
g
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
end;
theorem
:: GRFUNC_1:35
for
x
,
X
being ( ( ) ( )
set
)
for
g
,
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
c=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) &
x
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
X
: ( ( ) ( )
set
)
/\
(
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
c=
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;