:: 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 b2 : ( ( 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(b2 : ( ( 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 ) ;