:: EQUATION semantic presentation

begin

theorem :: EQUATION:1
for A being ( ( ) ( ) set )
for B, C being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of A : ( ( ) ( ) set ) ,B : ( ( non empty ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of B : ( ( non empty ) ( non empty ) set ) ,C : ( ( non empty ) ( non empty ) set ) ) st rng (g : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:b1 : ( ( ) ( ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b3 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = C : ( ( non empty ) ( non empty ) set ) holds
rng g : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool b3 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = C : ( ( non empty ) ( non empty ) set ) ;

theorem :: EQUATION:2
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B, C being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for f being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for g being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,C : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st g : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** f : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" holds
g : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" ;

theorem :: EQUATION:3
for A, B being ( ( non empty ) ( non empty ) set )
for C, y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in Funcs (A : ( ( non empty ) ( non empty ) set ) ,(Funcs (B : ( ( non empty ) ( non empty ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) & y : ( ( ) ( ) set ) in B : ( ( non empty ) ( non empty ) set ) holds
( dom ((commute f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding Relation-yielding ) set ) . y : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = A : ( ( non empty ) ( non empty ) set ) & rng ((commute f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding Relation-yielding ) set ) . y : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) c= C : ( ( ) ( ) set ) ) ;

theorem :: EQUATION:4
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is_transformable_to B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
for f being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of I : ( ( ) ( ) set ) ) st doms f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) & rngs f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) c= B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) is ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: EQUATION:5
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for C, E being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for D being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of C : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) st E : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = D : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b5 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) holds
(F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || C : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b5 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || D : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b5 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b7 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b5 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || E : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b6 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: EQUATION:6
for I being ( ( ) ( ) set )
for B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for C being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for A being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of C : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ex G being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of C : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) || A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b4 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b4 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

definition
let I be ( ( ) ( ) set ) ;
let A be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
let F be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of I : ( ( ) ( ) set ) ) ;
func F "" A -> ( ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) 1-sorted ) ) means :: EQUATION:def 1
 for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( ) ( ) 1-sorted ) holds
it : ( ( Function-like quasi_total ) ( Relation-like A : ( ( ) ( ) ClosureStr over I : ( ( ) ( ) 1-sorted ) ) -defined I : ( ( ) ( ) 1-sorted ) -valued Function-like quasi_total ) Element of bool [:A : ( ( ) ( ) ClosureStr over I : ( ( ) ( ) 1-sorted ) ) ,I : ( ( ) ( ) 1-sorted ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (F : ( ( ) ( functional ) Element of bool (Bool A : ( ( ) ( ) ClosureStr over I : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) " (A : ( ( ) ( ) ClosureStr over I : ( ( ) ( ) 1-sorted ) ) . i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;
end;

theorem :: EQUATION:7
for I being ( ( ) ( ) set )
for A, B, C being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .:.: C : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) is ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: EQUATION:8
for I being ( ( ) ( ) set )
for A, B, C being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "" C : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: EQUATION:9
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" holds
F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .:.: A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ;

theorem :: EQUATION:10
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is_transformable_to B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "" B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) = A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ;

theorem :: EQUATION:11
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) c= rngs F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) holds
F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) .:.: (F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) "" A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ;

theorem :: EQUATION:12
for I being ( ( ) ( ) set )
for f being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of I : ( ( ) ( ) set ) )
for X being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) .:.: X : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) c= rngs f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ;

theorem :: EQUATION:13
for I being ( ( ) ( ) set )
for f being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of I : ( ( ) ( ) set ) ) holds f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) .:.: (doms f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = rngs f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ;

theorem :: EQUATION:14
for I being ( ( ) ( ) set )
for f being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of I : ( ( ) ( ) set ) ) holds f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) "" (rngs f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) = doms f : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ;

theorem :: EQUATION:15
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds (id A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding "1-1" "onto" ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .:.: A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ;

theorem :: EQUATION:16
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds (id A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding "1-1" "onto" ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "" A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) = A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ;

begin

theorem :: EQUATION:17
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for A being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) holds A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of MSAlgebra(# the Sorts of A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the Charact of A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier' of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of the Arity of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like non empty total quasi_total Function-yielding Relation-yielding ) Element of bool [: the carrier' of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the ResultSort of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier' of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ;

theorem :: EQUATION:18
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for A being ( ( ) ( ) MSSubAlgebra of U0 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) set ) in Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,U0 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: EQUATION:19
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for A being ( ( ) ( ) MSSubAlgebra of U0 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) holds
(Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) )) : ( ( Function-like quasi_total ) ( Relation-like Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 the Sorts of b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Element of bool [:(Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) )) : ( ( ) ( ) Element of proj2 ( the Sorts of b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) )) : ( ( ) ( ) Element of proj2 the Sorts of b3 : ( ( ) ( ) MSSubAlgebra of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,U0 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )) : ( ( Function-like quasi_total ) ( Relation-like Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( ) Element of proj2 the Sorts of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Element of bool [:(Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )) : ( ( ) ( ) Element of proj2 ( the Sorts of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )) : ( ( ) ( ) Element of proj2 the Sorts of b2 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: EQUATION:20
for I being ( ( ) ( ) set )
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of I : ( ( ) ( ) set ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for B being ( ( ) ( ) MSSubAlgebra of product F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b4 : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) holds
( (Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) )) : ( ( Function-like quasi_total ) ( Relation-like Args (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b4 : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 the Sorts of b4 : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Element of bool [:(Args (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) )) : ( ( ) ( ) Element of proj2 ( the Sorts of b4 : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) )) : ( ( ) ( ) Element of proj2 the Sorts of b4 : ( ( ) ( ) MSSubAlgebra 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 feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) & (Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(product F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )) : ( ( Function-like quasi_total ) ( Relation-like Args (b5 : ( ( ) ( ) 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 feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of proj2 ( 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 feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b5 : ( ( ) ( ) 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 feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of proj2 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 feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V155() ) set ) ) -valued Function-like non empty total quasi_total ) Element of bool [:(Args (b5 : ( ( ) ( ) 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 feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )) : ( ( ) ( functional non empty ) Element of proj2 ( 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 feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b5 : ( ( ) ( ) 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 feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of proj2 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 feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V155() ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) ;

definition
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
let A be ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
let B be ( ( ) ( ) MSSubAlgebra of A : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ;
func SuperAlgebraSet B -> ( ( ) ( ) set ) means :: EQUATION:def 2
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( Function-like quasi_total ) ( Relation-like A : ( ( ) ( ) ClosureStr over S : ( ( ) ( ) 1-sorted ) ) -defined S : ( ( ) ( ) 1-sorted ) -valued Function-like quasi_total ) Element of bool [:A : ( ( ) ( ) ClosureStr over S : ( ( ) ( ) 1-sorted ) ) ,S : ( ( ) ( ) 1-sorted ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) iff ex C being ( ( strict ) ( strict ) MSSubAlgebra of A : ( ( ) ( ) ClosureStr over S : ( ( ) ( ) 1-sorted ) ) ) st
( x : ( ( ) ( ) set ) = C : ( ( strict ) ( strict ) MSSubAlgebra of A : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) & B : ( ( ) ( functional ) Element of bool (Bool A : ( ( ) ( ) ClosureStr over S : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) MSSubAlgebra of C : ( ( strict ) ( strict ) MSSubAlgebra of A : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) ) );
end;

registration
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
let A be ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
let B be ( ( ) ( ) MSSubAlgebra of A : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ;
cluster SuperAlgebraSet B : ( ( ) ( ) MSSubAlgebra of A : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( ) set ) -> non empty ;
end;

registration
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
cluster strict non-empty free for ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
end;

registration
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
let A be ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
let X be ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) MSSubset of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
cluster GenMSAlg X : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( strict ) ( strict non-empty feasible ) MSSubAlgebra of A : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) -> strict finitely-generated ;
end;

registration
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
let A be ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
cluster strict non-empty finitely-generated for ( ( ) ( ) MSSubAlgebra of A : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ;
end;

registration
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
let A be ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
cluster feasible for ( ( ) ( ) MSSubAlgebra of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ;
end;

theorem :: EQUATION:21
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for A being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for C being ( ( ) ( ) MSSubAlgebra of A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )
for D being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSubset of the Sorts of A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) st D : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSubset of the Sorts of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) = the Sorts of C : ( ( ) ( ) MSSubAlgebra of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) holds
for h being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for g being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st g : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) = h : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) || D : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSubset of the Sorts of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b5 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSubset of the Sorts of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) , the Sorts of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) holds
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) Element of Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) )
for y being ( ( ) ( ) Element of Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,C : ( ( ) ( ) MSSubAlgebra of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b4 : ( ( ) ( ) MSSubAlgebra of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) st Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,C : ( ( ) ( ) MSSubAlgebra of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b4 : ( ( ) ( ) MSSubAlgebra of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() Function-yielding Relation-yielding FinSequence-like FinSubsequence-like FinSequence-membered ) set ) & x : ( ( ) ( ) Element of Args (b8 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) = y : ( ( ) ( ) Element of Args (b8 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) MSSubAlgebra of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b4 : ( ( ) ( ) MSSubAlgebra of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) holds
h : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) # x : ( ( ) ( ) Element of Args (b8 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) Element of Args (b8 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of proj2 ( the Sorts of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) = g : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) # y : ( ( ) ( ) Element of Args (b8 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) MSSubAlgebra of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) : ( ( ) ( ) Element of proj2 ( the Sorts of b4 : ( ( ) ( ) MSSubAlgebra of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) Element of Args (b8 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of proj2 ( the Sorts of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) M8( the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: EQUATION:22
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for A being ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for C being ( ( feasible ) ( feasible ) MSSubAlgebra of A : ( ( feasible ) ( feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )
for D being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) st D : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSubset of the Sorts of b3 : ( ( feasible ) ( feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) = the Sorts of C : ( ( feasible ) ( feasible ) MSSubAlgebra of b3 : ( ( feasible ) ( feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) holds
for h being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st h : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is_homomorphism A : ( ( feasible ) ( feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) holds
for g being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st g : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) = h : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) || D : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSubset of the Sorts of b3 : ( ( feasible ) ( feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b5 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSubset of the Sorts of b3 : ( ( feasible ) ( feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) , the Sorts of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) holds
g : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is_homomorphism C : ( ( feasible ) ( feasible ) MSSubAlgebra of b3 : ( ( feasible ) ( feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ,U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;

theorem :: EQUATION:23
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for B being ( ( strict non-empty ) ( strict non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for G being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )
for H being ( ( V2() ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of B : ( ( strict non-empty ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )
for f being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st H : ( ( V2() ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of b3 : ( ( strict non-empty ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) c= f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) .:.: G : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) GeneratorSet of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) & f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is_homomorphism U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,B : ( ( strict non-empty ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) holds
f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is_epimorphism U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,B : ( ( strict non-empty ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;

theorem :: EQUATION:24
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0, U1 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for W being ( ( strict non-empty free ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for F being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st F : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is_epimorphism U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,U1 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) holds
for G being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st G : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is_homomorphism W : ( ( strict non-empty free ) ( strict non-empty free feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,U1 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) holds
ex H being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st
( H : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is_homomorphism W : ( ( strict non-empty free ) ( strict non-empty free feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) & G : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) = F : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ** H : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like Function-yielding Relation-yielding ) set ) ) ;

theorem :: EQUATION:25
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for I being ( ( non empty finite ) ( non empty finite ) set )
for A being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for F being ( ( ) ( Relation-like b2 : ( ( non empty finite ) ( non empty finite ) set ) -defined Function-like non empty total ) MSAlgebra-Family of I : ( ( non empty finite ) ( non empty finite ) set ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st ( for i being ( ( ) ( ) Element of I : ( ( non empty finite ) ( non empty finite ) set ) ) ex C being ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of A : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) st C : ( ( ) ( ) Element of b2 : ( ( non empty finite ) ( non empty finite ) set ) ) = F : ( ( ) ( Relation-like b2 : ( ( non empty finite ) ( non empty finite ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b2 : ( ( non empty finite ) ( non empty finite ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) . i : ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of b3 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) holds
ex B being ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of A : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) st
for i being ( ( ) ( ) Element of I : ( ( non empty finite ) ( non empty finite ) set ) ) holds F : ( ( ) ( Relation-like b2 : ( ( non empty finite ) ( non empty finite ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b2 : ( ( non empty finite ) ( non empty finite ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) . i : ( ( ) ( ) Element of b2 : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of B : ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of b3 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) ;

theorem :: EQUATION:26
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for A, B being ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ex M being ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) st
( A : ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) is ( ( ) ( ) MSSubAlgebra of M : ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) & B : ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) is ( ( ) ( ) MSSubAlgebra of M : ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) ) ;

theorem :: EQUATION:27
for SG being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for AG being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over SG : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for C being ( ( ) ( ) set ) st C : ( ( ) ( ) set ) = { A : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b3 : ( ( ) ( ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) where A is ( ( ) ( ) Element of MSSub AG : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) : ex R being ( ( strict non-empty finitely-generated ) ( strict non-empty finitely-generated feasible ) MSSubAlgebra of AG : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) st R : ( ( strict non-empty ) ( strict non-empty feasible ) MSSubAlgebra of product b4 : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b3 : ( ( ) ( ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) = A : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b3 : ( ( ) ( ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) } holds
for F being ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of C : ( ( ) ( ) set ) ,SG : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st ( for c being ( ( ) ( ) set ) st c : ( ( strict non-empty ) ( strict non-empty feasible ) MSSubAlgebra of product b4 : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b3 : ( ( ) ( ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) in C : ( ( ) ( ) set ) holds
c : ( ( strict non-empty ) ( strict non-empty feasible ) MSSubAlgebra of product b4 : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b3 : ( ( ) ( ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) = F : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b3 : ( ( ) ( ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) . c : ( ( strict non-empty ) ( strict non-empty feasible ) MSSubAlgebra of product b4 : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b3 : ( ( ) ( ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( ) set ) ) holds
ex PS being ( ( strict non-empty ) ( strict non-empty feasible ) MSSubAlgebra of product F : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b3 : ( ( ) ( ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ex BA being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of SG : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,SG : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st BA : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is_epimorphism PS : ( ( strict non-empty ) ( strict non-empty feasible ) MSSubAlgebra of product b4 : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b3 : ( ( ) ( ) set ) ,b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ,AG : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;

theorem :: EQUATION:28
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( free feasible ) ( free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for A being ( ( free ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total free ) GeneratorSet of U0 : ( ( free feasible ) ( free feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) )
for Z being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st Z : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) c= A : ( ( free ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total free ) GeneratorSet of b2 : ( ( free feasible ) ( free feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) & GenMSAlg Z : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( strict ) ( strict ) MSSubAlgebra of b2 : ( ( free feasible ) ( free feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) is feasible holds
GenMSAlg Z : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) MSSubset of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( strict ) ( strict ) MSSubAlgebra of b2 : ( ( free feasible ) ( free feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) is free ;

begin

definition
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
func TermAlg S -> ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) equals :: EQUATION:def 3
 FreeMSA ( the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) --> NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total ) Element of bool [: the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,(bool REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
end;

registration
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
cluster TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) -> strict non-empty free ;
end;

definition
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
func Equations S -> ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) equals :: EQUATION:def 4
[| the Sorts of (TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the Sorts of (TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) |] : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ;
end;

registration
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
cluster Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -> Relation-like V2() the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ;
end;

definition
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
mode EqualSet of S is ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSubset of Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ;
end;

notation
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
let s be ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ;
let x, y be ( ( ) ( ) Element of the Sorts of (TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
synonym x '=' y for [S,s];
end;

definition
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
let s be ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ;
let x, y be ( ( ) ( ) Element of the Sorts of (TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
:: original: '='
redefine func x '=' y -> ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . s : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: EQUATION:29
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for s being ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) )
for e being ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds e : ( ( ) ( ) Element of (Equations b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b2 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( ) set ) in the Sorts of (TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ;

theorem :: EQUATION:30
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for s being ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) )
for e being ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds e : ( ( ) ( ) Element of (Equations b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b2 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) in the Sorts of (TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ;

definition
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
let A be ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
let s be ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ;
let e be ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
pred A |= e means :: EQUATION:def 5
 for h being ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st h : ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) is_homomorphism TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) holds
(h : ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) . s : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the Sorts of (TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( ) ( ) set ) -defined the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:( the Sorts of (TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) ) : ( ( ) ( ) set ) ,( the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . (e : ( ( Function-like quasi_total ) ( Relation-like A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) -defined S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) -valued Function-like quasi_total ) Element of bool [:A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `1) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (h : ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) . s : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the Sorts of (TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( ) ( ) set ) -defined the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:( the Sorts of (TermAlg S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty free feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) ) : ( ( ) ( ) set ) ,( the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . s : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . (e : ( ( Function-like quasi_total ) ( Relation-like A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) -defined S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) -valued Function-like quasi_total ) Element of bool [:A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;
end;

definition
let S be ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ;
let A be ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
let E be ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;
pred A |= E means :: EQUATION:def 6
 for s being ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) )
for e being ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) st e : ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b1 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) in E : ( ( V2() V29() ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total V29() ) ManySortedSubset of the Sorts of A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( finite ) set ) holds
A : ( ( feasible ) ( feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= e : ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b1 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: EQUATION:31
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for s being ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) )
for e being ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) )
for U2 being ( ( strict non-empty ) ( strict non-empty feasible ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) st U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= e : ( ( ) ( ) Element of (Equations b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
U2 : ( ( strict non-empty ) ( strict non-empty feasible ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) |= e : ( ( ) ( ) Element of (Equations b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: EQUATION:32
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for E being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for U2 being ( ( strict non-empty ) ( strict non-empty feasible ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) st U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= E : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) holds
U2 : ( ( strict non-empty ) ( strict non-empty feasible ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) |= E : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;

theorem :: EQUATION:33
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0, U1 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for s being ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) )
for e being ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) st U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,U1 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) are_isomorphic & U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= e : ( ( ) ( ) Element of (Equations b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
U1 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= e : ( ( ) ( ) Element of (Equations b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b4 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: EQUATION:34
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0, U1 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for E being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,U1 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) are_isomorphic & U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= E : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) holds
U1 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= E : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;

theorem :: EQUATION:35
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for s being ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) )
for e being ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) )
for R being ( ( MSEquivalence-like MSCongruence-like ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Relation-yielding MSEquivalence-like MSCongruence-like ) MSCongruence of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= e : ( ( ) ( ) Element of (Equations b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
QuotMSAlg (U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,R : ( ( MSEquivalence-like MSCongruence-like ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Relation-yielding MSEquivalence-like MSCongruence-like ) MSCongruence of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= e : ( ( ) ( ) Element of (Equations b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: EQUATION:36
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty feasible ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for E being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for R being ( ( MSEquivalence-like MSCongruence-like ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Relation-yielding MSEquivalence-like MSCongruence-like ) MSCongruence of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= E : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) holds
QuotMSAlg (U0 : ( ( non-empty ) ( non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ,R : ( ( MSEquivalence-like MSCongruence-like ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Relation-yielding MSEquivalence-like MSCongruence-like ) MSCongruence of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= E : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of b1 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;

theorem :: EQUATION:37
for I being ( ( ) ( ) set )
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for s being ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) )
for e being ( ( ) ( ) Element of (Equations S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . s : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of I : ( ( ) ( ) set ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st ( for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) holds
ex A being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st
( A : ( ( ) ( ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) = F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) & A : ( ( ) ( ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= e : ( ( ) ( ) Element of (Equations b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) holds
product F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= e : ( ( ) ( ) Element of (Equations b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) . b3 : ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: EQUATION:38
for I being ( ( ) ( ) set )
for S being ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign )
for E being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of I : ( ( ) ( ) set ) ,S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st ( for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) holds
ex A being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) st
( A : ( ( ) ( ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) = F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) & A : ( ( ) ( ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= E : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ) ) holds
product F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) : ( ( ) ( strict non-empty feasible ) MSAlgebra over b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) |= E : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) EqualSet of b2 : ( ( non empty non void ) ( non empty non void feasible ) ManySortedSign ) ) ;