begin
begin
theorem
for
I being ( ( ) ( )
set )
for
A being ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
I : ( ( ) ( )
set ) )
for
B,
C being ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
I : ( ( ) ( )
set ) )
for
F being ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
A : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
B : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
for
G being ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
B : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
C : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
for
X being ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSubset of
A : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) holds
(G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b4 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
|| X : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSubset of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b7 : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSubset of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) ,
b4 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
= G : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b4 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
** (F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b7 : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSubset of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) ,
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b7 : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSubset of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) ,
b4 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) ;
begin
theorem
for
I being ( ( ) ( )
set )
for
A being ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
I : ( ( ) ( )
set ) )
for
B,
C being ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
I : ( ( ) ( )
set ) )
for
F being ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
A : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
B : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
for
G being ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
B : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
C : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
for
X being ( (
V2() ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSubset of
B : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) st
rngs F : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) : ( (
Relation-like Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
set )
c= X : ( (
V2() ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSubset of
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) holds
(G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V37() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || X : ( ( V2() ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b7 : ( (
V2() ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSubset of
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) ,
b4 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
** F : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) : ( (
Relation-like Function-like ) (
Relation-like Function-like Function-yielding V37() )
set )
= G : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b4 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
** F : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b4 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) ;
begin
theorem
for
I being ( ( ) ( )
set )
for
A being ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
I : ( ( ) ( )
set ) )
for
B being ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
I : ( ( ) ( )
set ) )
for
F being ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
A : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
B : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) holds
(
F : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) is
"onto" iff for
C being ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
I : ( ( ) ( )
set ) )
for
G,
H being ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
B : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
C : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) st
G : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b5 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
** F : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b5 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
= H : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b5 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
** F : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b5 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) holds
G : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b5 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
= H : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b5 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) ) ;
theorem
for
I being ( ( ) ( )
set )
for
A being ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
I : ( ( ) ( )
set ) )
for
B being ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
I : ( ( ) ( )
set ) )
for
F being ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
A : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
B : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) st
A : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) is
V2() holds
(
F : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) is
"1-1" iff for
C being ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
I : ( ( ) ( )
set ) )
for
G,
H being ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
C : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
A : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) st
F : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
** G : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b5 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) : ( (
Relation-like Function-like ) (
Relation-like Function-like Function-yielding V37() )
set )
= F : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b3 : ( (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like V2()
b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
** H : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b5 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) : ( (
Relation-like Function-like ) (
Relation-like Function-like Function-yielding V37() )
set ) holds
G : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b5 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) )
= H : ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total Function-yielding V37() )
ManySortedFunction of
b5 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ,
b2 : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
ManySortedSet of
b1 : ( ( ) ( )
set ) ) ) ) ;
begin
theorem
for
S being ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign )
for
U1 being ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
for
X being ( (
Relation-like V2() the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like V2() non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
ManySortedSet of the
carrier of
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )
for
h1,
h2 being ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) st
h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
is_homomorphism FreeMSA X : ( (
Relation-like V2() the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like V2() non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
ManySortedSet of the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ,
U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) &
h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
is_homomorphism FreeMSA X : ( (
Relation-like V2() the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like V2() non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
ManySortedSet of the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ,
U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) &
h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
|| (FreeGen X : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
GeneratorSet of
FreeMSA b3 : ( (
Relation-like V2() the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like V2() non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
ManySortedSet of the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
FreeGen b3 : ( (
Relation-like V2() the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like V2() non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
ManySortedSet of the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
GeneratorSet of
FreeMSA b3 : ( (
Relation-like V2() the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like V2() non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
ManySortedSet of the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ) , the
Sorts of
b2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) )
= h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
|| (FreeGen X : ( ( Relation-like V2() the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V51() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
GeneratorSet of
FreeMSA b3 : ( (
Relation-like V2() the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like V2() non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
ManySortedSet of the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
FreeGen b3 : ( (
Relation-like V2() the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like V2() non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
ManySortedSet of the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
GeneratorSet of
FreeMSA b3 : ( (
Relation-like V2() the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like V2() non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
ManySortedSet of the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ) , the
Sorts of
b2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) ) holds
h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
= h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ;
theorem
for
S being ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign )
for
U1,
U2 being ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
for
F being ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) st
F : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
is_epimorphism U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ,
U2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) holds
for
U3 being ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
for
h1,
h2 being ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) st
h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
** F : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of the
Sorts of
b2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) , the
Sorts of
b5 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) )
= h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
** F : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of the
Sorts of
b2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) , the
Sorts of
b5 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) ) holds
h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
= h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ;
theorem
for
S being ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign )
for
U2,
U3 being ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
for
F being ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) st
F : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
is_homomorphism U2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ,
U3 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) holds
(
F : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
is_monomorphism U2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ,
U3 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) iff for
U1 being ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
for
h1,
h2 being ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) st
h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
is_homomorphism U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ,
U2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) &
h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
is_homomorphism U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ,
U2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) &
F : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
** h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of the
Sorts of
b5 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) , the
Sorts of
b3 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) )
= F : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
** h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of the
Sorts of
b5 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) , the
Sorts of
b3 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) ) holds
h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
= h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ) ;
theorem
for
S being ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign )
for
U1,
U2 being ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
for
Gen being ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
GeneratorSet of
U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) )
for
h1,
h2 being ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) st
h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
is_homomorphism U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ,
U2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) &
h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
is_homomorphism U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ,
U2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) &
h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
|| Gen : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
GeneratorSet of
b2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b4 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
GeneratorSet of
b2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ) , the
Sorts of
b3 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) )
= h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
|| Gen : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
GeneratorSet of
b2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ) : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b4 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
GeneratorSet of
b2 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ) , the
Sorts of
b3 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) (
Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total )
set ) ) holds
h1 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) )
= h2 : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like non
empty total Function-yielding V37() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V51() )
ManySortedSign ) ) ;