begin
begin
begin
theorem
for
S being ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign)
for
U0 being ( (
order-sorted ) (
order-sorted )
OSAlgebra of
S : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) )
for
U1 being ( ( ) ( )
MSAlgebra over
S : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) holds
(
U1 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) is ( (
order-sorted ) (
order-sorted )
OSSubAlgebra of
U0 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) iff ( the
Sorts of
U1 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set ) is ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
OSSubset of
U0 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) & ( for
B being ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
OSSubset of
U0 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) st
B : ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
OSSubset of
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) )
= the
Sorts of
U1 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set ) holds
(
B : ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
OSSubset of
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) is
opers_closed & the
Charact of
U1 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )
V75() )
ManySortedFunction of the
Arity of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( (
Function-like V21( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ))
-valued Function-like V21( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) )
Element of
K10(
K11( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ,
( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) : ( ( ) ( non
empty Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
* ( the Sorts of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ))
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ))
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) )
set ) : ( (
Relation-like ) ( non
empty Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set ) , the
ResultSort of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( (
Function-like V21( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-valued Function-like V21( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
Element of
K10(
K11( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
* the
Sorts of
b3 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set ) : ( (
Relation-like ) ( non
empty Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set ) )
= Opers (
U0 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ,
B : ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
OSSubset of
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) ) : ( ( ) ( non
empty Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )
V75() )
ManySortedFunction of the
Arity of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( (
Function-like V21( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ))
-valued Function-like V21( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) )
Element of
K10(
K11( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ,
( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) : ( ( ) ( non
empty Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
* (b4 : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) #) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ))
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ))
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) )
set ) : ( (
Relation-like ) ( non
empty Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set ) , the
ResultSort of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( (
Function-like V21( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-valued Function-like V21( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
Element of
K10(
K11( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
* b4 : ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
OSSubset of
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) : ( (
Relation-like ) ( non
empty Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set ) ) ) ) ) ) ;
begin
theorem
for
S1 being ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign)
for
OU0 being ( (
order-sorted ) (
order-sorted )
OSAlgebra of
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
A,
B being ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
OSSubset of
OU0 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) st
B : ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
OSSubset of
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) )
in OSSubSort A : ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
OSSubset of
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) : ( ( ) ( non
empty )
set ) holds
rng ((Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,OU0 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) )) : ( ( Function-like V21( Args (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) , Result (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Args (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V21( Args (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) , Result (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11((Args (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) )) : ( ( ) ( ) Element of rng ( the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) )) : ( ( ) ( ) Element of rng the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) | ((((OSMSubSort A : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) ) : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( Relation-like the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -valued Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) Element of K10(K11( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ,( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) . o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( (
Relation-like ) (
Relation-like (((OSMSubSort b4 : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) ) : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( Relation-like the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -valued Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) Element of K10(K11( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ,( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Relation-like ) ( non
empty Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set )
. b3 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
-defined Args (
b3 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) : ( ( ) ( )
Element of
rng ( the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ))
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ))
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) )
set ) : ( ( ) ( non
empty )
set ) )
-defined Result (
b3 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) : ( ( ) ( )
Element of
rng the
Sorts of
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like )
set ) : ( ( ) ( )
set )
c= (B : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) * the ResultSort of S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Relation-like ) ( non
empty Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set )
. o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ;
theorem
for
S1 being ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign)
for
OU0 being ( (
order-sorted ) (
order-sorted )
OSAlgebra of
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
A being ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
OSSubset of
OU0 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) holds
rng ((Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,OU0 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) )) : ( ( Function-like V21( Args (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) , Result (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Args (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V21( Args (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) , Result (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( ) Element of rng the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11((Args (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) )) : ( ( ) ( ) Element of rng ( the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b3 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) )) : ( ( ) ( ) Element of rng the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) | ((((OSMSubSort A : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) ) : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( Relation-like the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -valued Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) Element of K10(K11( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ,( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) . o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( (
Relation-like ) (
Relation-like (((OSMSubSort b4 : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) ) : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) ( Relation-like the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) -valued Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) ) Element of K10(K11( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ,( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional V81() ) M12( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Relation-like ) ( non
empty Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set )
. b3 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
-defined Args (
b3 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) : ( ( ) ( )
Element of
rng ( the Sorts of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ))
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ))
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
* : ( ( ) ( non
empty functional V81() )
M12( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) )) ) )
set ) : ( ( ) ( non
empty )
set ) )
-defined Result (
b3 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ) : ( ( ) ( )
Element of
rng the
Sorts of
b2 : ( (
order-sorted ) (
order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like )
set ) : ( ( ) ( )
set )
c= ((OSMSubSort A : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) ) : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) OSSubset of b2 : ( ( order-sorted ) ( order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) * the ResultSort of S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier' of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Relation-like ) ( non
empty Relation-like the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set )
-defined Function-like V17( the
carrier' of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) : ( ( ) ( non
empty )
set ) ) )
set )
. o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ;
begin
begin
theorem
for
S1 being ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign)
for
U0 being ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) )
for
x,
y being ( ( ) ( )
Element of
OSSub U0 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) holds
(OSAlg_meet U0 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( (
Function-like V21(
K11(
(OSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ,
(OSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set ) ,
OSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) ) (
Relation-like K11(
(OSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ,
(OSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set )
-defined OSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) )
-valued Function-like V21(
K11(
(OSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ,
(OSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set ) ,
OSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) )
BinOp of
OSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) )
. (
x : ( ( ) ( )
Element of
OSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) ,
y : ( ( ) ( )
Element of
OSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) ) : ( ( ) ( )
Element of
OSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) )
= (MSAlg_meet U0 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( (
Function-like V21(
K11(
(MSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
set ) ,
(MSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty Relation-like )
set ) ,
MSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like K11(
(MSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
set ) ,
(MSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty Relation-like )
set )
-defined MSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
set )
-valued Function-like V21(
K11(
(MSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
set ) ,
(MSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty Relation-like )
set ) ,
MSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
set ) ) )
Element of
K10(
K11(
K11(
(MSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
set ) ,
(MSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty Relation-like )
set ) ,
(MSSub b2 : ( ( non-empty order-sorted ) ( non-empty order-sorted ) OSAlgebra of b1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OrderSortedSign) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
. (
x : ( ( ) ( )
Element of
OSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) ,
y : ( ( ) ( )
Element of
OSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) ) : ( ( ) ( )
Element of
MSSub b2 : ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
b1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) : ( ( ) ( non
empty )
set ) ) ;
definition
let S1 be ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ;
let U0 be ( (
non-empty order-sorted ) (
non-empty order-sorted )
OSAlgebra of
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OrderSortedSign) ) ;
func OSSubAlLattice U0 -> ( ( non
empty strict Lattice-like ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like )
Lattice)
equals
LattStr(#
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ,
(OSAlg_join U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( (
Function-like V21(
K11(
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ,
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set ) ,
OSSub U0 : ( (
order-sorted ) (
order-sorted )
MSAlgebra over
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OverloadedRSSign ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) ) (
Relation-like K11(
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ,
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set )
-defined OSSub U0 : ( (
order-sorted ) (
order-sorted )
MSAlgebra over
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OverloadedRSSign ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) )
-valued Function-like V21(
K11(
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ,
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set ) ,
OSSub U0 : ( (
order-sorted ) (
order-sorted )
MSAlgebra over
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OverloadedRSSign ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) )
BinOp of
OSSub U0 : ( (
order-sorted ) (
order-sorted )
MSAlgebra over
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OverloadedRSSign ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) ,
(OSAlg_meet U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( (
Function-like V21(
K11(
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ,
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set ) ,
OSSub U0 : ( (
order-sorted ) (
order-sorted )
MSAlgebra over
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OverloadedRSSign ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) ) (
Relation-like K11(
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ,
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set )
-defined OSSub U0 : ( (
order-sorted ) (
order-sorted )
MSAlgebra over
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OverloadedRSSign ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) )
-valued Function-like V21(
K11(
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ,
(OSSub U0 : ( ( order-sorted ) ( order-sorted ) MSAlgebra over S1 : ( ( non empty non void order-sorted discernable ) ( non empty non void V52() V99() V100() V101() order-sorted discernable ) OverloadedRSSign ) ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set ) ,
OSSub U0 : ( (
order-sorted ) (
order-sorted )
MSAlgebra over
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OverloadedRSSign ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) )
BinOp of
OSSub U0 : ( (
order-sorted ) (
order-sorted )
MSAlgebra over
S1 : ( ( non
empty non
void order-sorted discernable ) ( non
empty non
void V52()
V99()
V100()
V101()
order-sorted discernable )
OverloadedRSSign ) ) : ( ( ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) ) ) #) : ( (
strict ) ( non
empty strict )
LattStr ) ;
end;