begin
begin
definition
let S be ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ;
let U0 be ( ( ) ( )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ;
let o be ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ;
func const (
o,
U0)
-> ( ( ) ( )
set )
equals
(Den (o : ( ( ) ( Relation-like S : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of S : ( ( ) ( ) set ) ,U0 : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like Args (
o : ( ( ) (
Relation-like S : ( ( ) ( )
set )
-defined Function-like total )
MSAlgebra-Family of
S : ( ( ) ( )
set ) ,
U0 : ( ( ) ( )
set ) ) ,
U0 : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of
rng K186( the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set ) , the
Sorts of
U0 : ( ( ) ( )
set ) : ( (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
M10( the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
M10( the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) )
-defined Result (
o : ( ( ) (
Relation-like S : ( ( ) ( )
set )
-defined Function-like total )
MSAlgebra-Family of
S : ( ( ) ( )
set ) ,
U0 : ( ( ) ( )
set ) ) ,
U0 : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of
rng the
Sorts of
U0 : ( ( ) ( )
set ) : ( (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total )
set ) : ( ( ) ( )
set ) )
-valued Function-like quasi_total )
Element of
K10(
K11(
(Args (o : ( ( ) ( Relation-like S : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of S : ( ( ) ( ) set ) ,U0 : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( ) ( )
Element of
rng K186( the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set ) , the
Sorts of
U0 : ( ( ) ( )
set ) : ( (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
M10( the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
M10( the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ,
(Result (o : ( ( ) ( Relation-like S : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of S : ( ( ) ( ) set ) ,U0 : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( ) ( )
Element of
rng the
Sorts of
U0 : ( ( ) ( )
set ) : ( (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
. {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) : ( ( ) ( )
set ) ;
end;
theorem
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
U1,
U2 being ( ( ) ( )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
e being ( ( ) ( )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
U1 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( )
Element of
rng K186( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
b2 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) st
e : ( ( ) ( )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( )
Element of
rng K186( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
b2 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
= {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) &
the_arity_of o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) ))
= {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) &
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
U1 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( )
Element of
rng K186( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
b2 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) )
<> {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) &
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
U2 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( )
Element of
rng K186( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
b3 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) )
<> {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) holds
for
F being ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) holds
F : ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
# e : ( ( ) ( )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( )
Element of
rng K186( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
b2 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
b3 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( )
Element of
rng K186( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
b3 : ( ( ) ( )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
= {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) ;
begin
theorem
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
U1,
U2 being ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
F being ( ( ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
x being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
b3 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
for
n being ( ( ) ( )
set ) st
n : ( ( ) ( )
set )
in dom (the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) )) : ( ( ) (
countable )
Element of
K10(
K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) ) holds
(F : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total Function-yielding V54() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) # x : ( ( ) ( Relation-like Function-like ) Element of Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( non empty functional ) Element of rng K186( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like K183( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K183( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
Relation-like Function-like )
Element of
Args (
b2 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
b4 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
b4 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
. n : ( ( ) ( )
set ) : ( ( ) ( )
set )
= (F : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total Function-yielding V54() ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . ((the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K160() : ( ( ) ( V40() countable denumerable ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V70() ) M11( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,K183( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) )) /. n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
Sorts of
b3 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set )
. ((the_arity_of b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K160() : ( ( ) ( V40() countable denumerable ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V70() ) M11( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,K183( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) )) /. b7 : ( ( ) ( ) set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
-defined the
Sorts of
b4 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set )
. ((the_arity_of b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K160() : ( ( ) ( V40() countable denumerable ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V70() ) M11( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,K183( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) )) /. b7 : ( ( ) ( ) set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like quasi_total )
Element of
K10(
K11(
( the Sorts of b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . ((the_arity_of b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K160() : ( ( ) ( V40() countable denumerable ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V70() ) M11( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,K183( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) )) /. b7 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
set ) ,
( the Sorts of b4 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . ((the_arity_of b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K160() : ( ( ) ( V40() countable denumerable ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V70() ) M11( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,K183( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) )) /. b7 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
. (x : ( ( ) ( Relation-like Function-like ) Element of Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( non empty functional ) Element of rng K186( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like K183( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K183( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b1 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) . n : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( ( ) ( )
set ) ;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
x being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) holds
x : ( ( ) (
Relation-like Function-like )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
in Funcs (
(dom (the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K160() : ( ( ) ( V40() countable denumerable ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V70() ) M11( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,K183( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) )) ) : ( ( ) (
countable )
Element of
K10(
K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) ) ,
(Funcs (I : ( ( non empty ) ( non empty ) set ) ,(union { ( the Sorts of (A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . i9 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non-empty ) ( non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . s9 : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) where i9 is ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) , s9 is ( ( ) ( ) Element of the carrier of S : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : verum } ) : ( ( ) ( ) set ) )) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
x being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
for
n being ( ( ) ( )
set ) st
n : ( ( ) ( )
set )
in dom (the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) )) : ( ( ) (
countable )
Element of
K10(
K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) ) holds
x : ( ( ) (
Relation-like Function-like )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
. n : ( ( ) ( )
set ) : ( ( ) ( )
set )
in product (Carrier (A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ,((the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like K160() : ( ( ) ( V40() countable denumerable ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V70() ) M11( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,K183( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) )) /. n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) )) : ( (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
set ) : ( ( ) ( non
empty functional with_common_domain product-like )
set ) ;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
i being ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) )
for
n being ( ( ) ( )
set ) st
n : ( ( ) ( )
set )
in dom (the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) )) : ( ( ) (
countable )
Element of
K10(
K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) ) holds
for
s being ( ( ) ( )
SortSymbol of ( ( ) ( non
empty )
set ) ) st
s : ( ( ) ( )
SortSymbol of ( ( ) ( non
empty )
set ) )
= (the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) ))
. n : ( ( ) ( )
set ) : ( ( ) ( )
set ) holds
for
y being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
for
g being ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function) st
g : ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function)
= y : ( ( ) (
Relation-like Function-like )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
. n : ( ( ) ( )
set ) : ( ( ) ( )
set ) holds
g : ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function)
. i : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( )
set )
in the
Sorts of
(A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set )
. s : ( ( ) ( )
SortSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
y being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) st
the_arity_of o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) ))
<> {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) holds
commute y : ( ( ) (
Relation-like Function-like )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) : ( (
Relation-like Function-like Function-yielding ) (
Relation-like Function-like Function-yielding V54() )
set )
in product (doms (A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ?. o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total Function-yielding ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total Function-yielding V54() ) set ) ) : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) (
functional with_common_domain product-like )
set ) ;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
y being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) st
the_arity_of o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) ))
<> {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) holds
y : ( ( ) (
Relation-like Function-like )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
in dom (Commute (Frege (A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ?. o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total Function-yielding ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total Function-yielding V54() ) set ) ) : ( ( Relation-like product (doms (b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ?. b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total Function-yielding ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total Function-yielding V54() ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( functional with_common_domain product-like ) set ) -defined Function-like total Function-yielding ) ( Relation-like product (doms (b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ?. b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total Function-yielding ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total Function-yielding V54() ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( functional with_common_domain product-like ) set ) -defined Function-like total Function-yielding V54() ) set ) ) : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) ;
theorem
for
I being ( ( ) ( )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( ) ( )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
x being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) holds
(Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) )) : ( (
Function-like quasi_total ) (
Relation-like Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) )
-defined Result (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty )
Element of
rng the
Sorts of
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) : ( ( ) ( non
empty with_non-empty_elements non
empty-membered )
set ) )
-valued Function-like quasi_total )
Element of
K10(
K11(
(Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) )) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ,
(Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) )) : ( ( ) ( non
empty )
Element of
rng the
Sorts of
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) : ( ( ) ( non
empty with_non-empty_elements non
empty-membered )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
. x : ( ( ) (
Relation-like Function-like )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
Element of
Result (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty )
Element of
rng the
Sorts of
(product b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) : ( ( ) ( non
empty with_non-empty_elements non
empty-membered )
set ) ) )
in product (Carrier (A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ,(the_result_sort_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) )) : ( (
Relation-like b1 : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like non-empty b1 : ( ( ) ( )
set )
-defined Function-like total )
set ) : ( ( ) ( non
empty functional with_common_domain product-like )
set ) ;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
i being ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) st
the_arity_of o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) ))
<> {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) holds
for
U1 being ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
x being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) holds
(commute x : ( ( ) ( Relation-like Function-like ) Element of Args (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( non empty functional ) Element of rng K186( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of (product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like K183( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K183( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Relation-like Function-like Function-yielding ) (
Relation-like Function-like Function-yielding V54() )
set )
. i : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
Relation-like Function-like )
set ) is ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b4 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) ;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
i being ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
x being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
for
n being ( ( ) ( )
set ) st
n : ( ( ) ( )
set )
in dom (the_arity_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) )) : ( ( ) (
countable )
Element of
K10(
K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) ) holds
for
f being ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function) st
f : ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function)
= x : ( ( ) (
Relation-like Function-like )
Element of
Args (
b5 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
. n : ( ( ) ( )
set ) : ( ( ) ( )
set ) holds
((commute x : ( ( ) ( Relation-like Function-like ) Element of Args (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( non empty functional ) Element of rng K186( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of (product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like K183( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K183( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V54() ) set ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like Function-like )
set )
. n : ( ( ) ( )
set ) : ( ( ) ( )
set )
= f : ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function)
. i : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) st
the_arity_of o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) ))
<> {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) holds
for
y being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
for
i9 being ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) )
for
g being ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function) st
g : ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function)
= (Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) )) : ( (
Function-like quasi_total ) (
Relation-like Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) )
-defined Result (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty )
Element of
rng the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) : ( ( ) ( non
empty with_non-empty_elements non
empty-membered )
set ) )
-valued Function-like quasi_total )
Element of
K10(
K11(
(Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) )) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ,
(Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) )) : ( ( ) ( non
empty )
Element of
rng the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) : ( ( ) ( non
empty with_non-empty_elements non
empty-membered )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
. y : ( ( ) (
Relation-like Function-like )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
Element of
Result (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty )
Element of
rng the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) : ( ( ) ( non
empty with_non-empty_elements non
empty-membered )
set ) ) ) holds
g : ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function)
. i9 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( )
set )
= (Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . i9 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non-empty ) ( non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) )) : ( (
Function-like quasi_total ) (
Relation-like Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b6 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b6 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) )
-defined Result (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b6 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty )
Element of
rng the
Sorts of
(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b6 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) : ( ( ) ( non
empty with_non-empty_elements non
empty-membered )
set ) )
-valued Function-like quasi_total )
Element of
K10(
K11(
(Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b6 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non-empty ) ( non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) )) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b6 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ,
(Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b6 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non-empty ) ( non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) )) : ( ( ) ( non
empty )
Element of
rng the
Sorts of
(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b6 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) : ( ( ) ( non
empty with_non-empty_elements non
empty-membered )
set ) ) ) : ( ( ) ( non
empty Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
. ((commute y : ( ( ) ( Relation-like Function-like ) Element of Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( non empty functional ) Element of rng K186( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of (product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like K183( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K183( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V54() ) set ) . i9 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) ;
begin
definition
let I be ( ( non
empty ) ( non
empty )
set ) ;
let S be ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ;
let A be ( ( ) ( non
empty Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ;
let i be ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) ;
func proj (
A,
i)
-> ( ( ) ( non
empty Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
S : ( ( ) ( )
set ) ,
S : ( ( ) ( )
set ) )
means
for
s being ( ( ) ( )
Element of ( ( ) ( )
set ) ) holds
it : ( ( ) ( non
empty Relation-like the
carrier of
I : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of the
Sorts of
S : ( ( ) ( )
set ) : ( (
Relation-like the
carrier of
I : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like the
carrier of
I : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total )
set ) , the
Sorts of
A : ( ( ) ( )
Element of the
carrier' of
I : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Relation-like the
carrier of
I : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like the
carrier of
I : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total )
set ) )
. s : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( (
Function-like quasi_total ) (
Relation-like the
Sorts of
(product A : ( ( ) ( ) Element of the carrier' of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
MSAlgebra over
S : ( ( ) ( )
set ) ) : ( (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total )
set )
. b1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
-defined the
Sorts of
(A : ( ( ) ( ) Element of the carrier' of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . i : ( ( ) ( non empty Relation-like S : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of S : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( ) ( )
set ) ) : ( (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like the
carrier of
S : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total )
set )
. b1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
K10(
K11(
( the Sorts of (product A : ( ( ) ( ) Element of the carrier' of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) MSAlgebra over S : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
set ) ,
( the Sorts of (A : ( ( ) ( ) Element of the carrier' of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . i : ( ( ) ( non empty Relation-like S : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of S : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) ) ) : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like total ) set ) . b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
set ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
= proj (
(Carrier (A : ( ( ) ( ) Element of the carrier' of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( (
Relation-like I : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like I : ( ( ) ( )
set )
-defined Function-like total )
set ) ,
i : ( ( ) ( non
empty Relation-like S : ( ( ) ( )
set )
-defined Function-like total )
MSAlgebra-Family of
S : ( ( ) ( )
set ) ,
I : ( ( ) ( )
set ) ) ) : ( (
Relation-like Function-like ) (
Relation-like product (Carrier (A : ( ( ) ( ) Element of the carrier' of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( (
Relation-like I : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like I : ( ( ) ( )
set )
-defined Function-like total )
set ) : ( ( ) (
functional with_common_domain product-like )
set )
-defined Function-like total )
set ) ;
end;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
o being ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) )
for
x being ( ( ) (
Relation-like Function-like )
Element of
Args (
o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) st
the_arity_of o : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like K160() : ( ( ) (
V40()
countable denumerable )
Element of
K10(
K156() : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-valued Function-like V70() )
M11( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ,
K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) )) ))
<> {} : ( ( ) (
empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Cardinal-yielding Function-yielding V54() )
set ) holds
for
i being ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) holds
(proj (A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ,i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
# x : ( ( ) (
Relation-like Function-like )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like )
Element of
Args (
b4 : ( ( ) ( )
OperSymbol of ( ( ) ( non
empty )
set ) ) ,
(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b6 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) : ( ( ) ( non
empty functional )
Element of
rng K186( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) , the
Sorts of
(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b6 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) ) : ( (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total ) (
Relation-like K183( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M10( the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set ) ))
-defined Function-like total )
set ) : ( ( ) ( )
set ) ) )
= (commute x : ( ( ) ( Relation-like Function-like ) Element of Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( non empty functional ) Element of rng K186( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of (product b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like K183( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K183( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M10( the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Relation-like Function-like Function-yielding ) (
Relation-like Function-like Function-yielding V54() )
set )
. i : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
Relation-like Function-like )
set ) ;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
i being ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
s being ( ( ) ( )
SortSymbol of ( ( ) ( non
empty )
set ) )
for
U1 being ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
F being ( (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
I : ( ( non
empty ) ( non
empty )
set ) ) st ( for
i being ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) ex
F1 being ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) st
(
F1 : ( ( ) ( )
set )
= F : ( (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b1 : ( ( non
empty ) ( non
empty )
set ) )
. i : ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( ( ) (
Relation-like Function-like )
set ) &
F1 : ( ( ) ( )
set )
is_homomorphism U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ,
A : ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
. i : ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) ) holds
for
F9 being ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) st
F9 : ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
= F : ( (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b1 : ( ( non
empty ) ( non
empty )
set ) )
. i : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
Relation-like Function-like )
set ) holds
for
x being ( ( ) ( )
set ) st
x : ( ( ) ( )
set )
in the
Sorts of
U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set )
. s : ( ( ) ( )
SortSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) holds
for
f being ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function) st
f : ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function)
= (commute ((commute F : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total Function-yielding ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total Function-yielding V54() ) ManySortedFunction of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V54() ) set ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like ) set ) ) : ( (
Relation-like Function-like Function-yielding ) (
Relation-like Function-like Function-yielding V54() )
set )
. x : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set ) holds
f : ( (
Relation-like Function-like ) (
Relation-like Function-like )
Function)
. i : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( )
set )
= (F9 : ( ( ) ( non empty Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total Function-yielding V54() ) ManySortedFunction of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
Sorts of
b6 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set )
. b5 : ( ( ) ( )
SortSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-defined the
Sorts of
(b4 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set )
. b5 : ( ( ) ( )
SortSymbol of ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set )
-valued Function-like quasi_total )
Element of
K10(
K11(
( the Sorts of b6 : ( ( non-empty ) ( non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . b5 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non
empty )
set ) ,
( the Sorts of (b4 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non-empty ) ( non-empty ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) set ) . b5 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) )
. x : ( ( ) ( )
set ) : ( ( ) ( )
set ) ;
theorem
for
I being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign )
for
A being ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
U1 being ( (
non-empty ) (
non-empty )
MSAlgebra over
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
for
F being ( (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
I : ( ( non
empty ) ( non
empty )
set ) ) st ( for
i being ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) ex
F1 being ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) st
(
F1 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
= F : ( (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b1 : ( ( non
empty ) ( non
empty )
set ) )
. i : ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( ( ) (
Relation-like Function-like )
set ) &
F1 : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
is_homomorphism U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ,
A : ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
. i : ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ) ) holds
ex
H being ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) st
(
H : ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
is_homomorphism U1 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ,
product A : ( ( ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( ( ) (
strict non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) & ( for
i being ( ( ) ( )
Element of
I : ( ( non
empty ) ( non
empty )
set ) ) holds
(proj (A : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) ,i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) )
** H : ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ,
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of the
Sorts of
b4 : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) , the
Sorts of
(b3 : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty non void ) ( non empty non void V68() ) ManySortedSign ) ) . b7 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
non-empty ) (
non-empty )
MSAlgebra over
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) : ( (
Relation-like the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total ) ( non
empty Relation-like non-empty non
empty-yielding the
carrier of
b2 : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) : ( ( ) ( non
empty )
set )
-defined Function-like total )
set ) )
= F : ( (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding ) ( non
empty Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of
b1 : ( ( non
empty ) ( non
empty )
set ) )
. i : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
Relation-like Function-like )
set ) ) ) ;
begin
definition
let I be ( ( non
empty ) ( non
empty )
set ) ;
let S be ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ;
let A be ( ( ) ( non
empty Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined Function-like total )
MSAlgebra-Family of
I : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty non
void ) ( non
empty non
void V68() )
ManySortedSign ) ) ;
let EqR be ( (
V14()
V19()
total ) (
Relation-like I : ( ( non
empty ) ( non
empty )
set )
-defined I : ( ( non
empty ) ( non
empty )
set )
-valued V12()
V14()
V19()
total )
Equivalence_Relation of
I : ( ( non
empty ) ( non
empty )
set ) ) ;
func A / EqR -> ( ( ) ( non
empty Relation-like Class EqR : ( ( ) ( non
empty Relation-like S : ( ( ) ( )
set )
-defined Function-like total )
MSAlgebra-Family of
S : ( ( ) ( )
set ) ,
I : ( ( ) ( )
set ) ) : ( ( ) (
with_non-empty_elements )
a_partition of
I : ( ( ) ( )
set ) )
-defined Function-like total )
MSAlgebra-Class of
S : ( ( ) ( )
set ) ,
id (Class EqR : ( ( ) ( non empty Relation-like S : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of S : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) ) ) : ( ( ) (
with_non-empty_elements )
a_partition of
I : ( ( ) ( )
set ) ) : ( (
total ) (
Relation-like non-empty Class EqR : ( ( ) ( non
empty Relation-like S : ( ( ) ( )
set )
-defined Function-like total )
MSAlgebra-Family of
S : ( ( ) ( )
set ) ,
I : ( ( ) ( )
set ) ) : ( ( ) (
with_non-empty_elements )
a_partition of
I : ( ( ) ( )
set ) )
-defined Class EqR : ( ( ) ( non
empty Relation-like S : ( ( ) ( )
set )
-defined Function-like total )
MSAlgebra-Family of
S : ( ( ) ( )
set ) ,
I : ( ( ) ( )
set ) ) : ( ( ) (
with_non-empty_elements )
a_partition of
I : ( ( ) ( )
set ) )
-valued V12()
V14()
V15()
V19()
Function-like one-to-one total )
Element of
K10(
K11(
(Class EqR : ( ( ) ( non empty Relation-like S : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of S : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) ) ) : ( ( ) (
with_non-empty_elements )
a_partition of
I : ( ( ) ( )
set ) ) ,
(Class EqR : ( ( ) ( non empty Relation-like S : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of S : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) ) ) : ( ( ) (
with_non-empty_elements )
a_partition of
I : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( non
empty )
set ) ) )
means
for
c being ( ( ) ( )
set ) st
c : ( ( ) ( )
set )
in Class EqR : ( ( ) ( non
empty Relation-like S : ( ( ) ( )
set )
-defined Function-like total )
MSAlgebra-Family of
S : ( ( ) ( )
set ) ,
I : ( ( ) ( )
set ) ) : ( ( ) (
with_non-empty_elements )
a_partition of
I : ( ( ) ( )
set ) ) holds
it : ( ( ) ( non
empty Relation-like the
carrier of
I : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total Function-yielding V54() )
ManySortedFunction of the
Sorts of
S : ( ( ) ( )
set ) : ( (
Relation-like the
carrier of
I : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like the
carrier of
I : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total )
set ) , the
Sorts of
A : ( ( ) ( )
Element of the
carrier' of
I : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Relation-like the
carrier of
I : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total ) (
Relation-like the
carrier of
I : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined Function-like total )
set ) )
. c : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set )
= A : ( ( ) ( )
Element of the
carrier' of
I : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
| c : ( ( ) ( )
set ) : ( (
Relation-like ) (
Relation-like )
set ) ;
end;