let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;

let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;

let S be ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ;
let A be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ;
let o be ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ;

let S be ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ;
let I be ( ( ) ( ) set ) ;
let s be ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) MSAlgebra-Family of I : ( ( ) ( ) set ) ,S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ;

let S be ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ;
let X be ( ( Relation-like V2() the carrier of S : ( ( non empty non void ) ( non empty non void V54() ) 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 V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ;

let S be ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ;
let X be ( ( Relation-like V2() the carrier of S : ( ( non empty non void ) ( non empty non void V54() ) 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 V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ;

let S be ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ;
let A, B be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ;

for a, X, Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st a : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . a : ( ( ) ( ) set ) : ( ( ) ( ) set ) in [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . a : ( ( ) ( ) set ) : ( ( ) ( ) set ) = [((pr1 f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,((pr2 f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) ;

for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( ) ( ) set )
for f being ( ( Function-like V18(b₁ : ( ( non empty ) ( non empty ) set ) ,{b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) ) ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined {b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) -valued Function-like non empty total V18(b₁ : ( ( non empty ) ( non empty ) set ) ,{b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) ) ) Function of X : ( ( non empty ) ( non empty ) set ) ,{Y : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) ) holds rng f : ( ( Function-like V18(b₁ : ( ( non empty ) ( non empty ) set ) ,{b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) ) ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined {b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) -valued Function-like non empty total V18(b₁ : ( ( non empty ) ( non empty ) set ) ,{b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) ) ) Function of b₁ : ( ( non empty ) ( non empty ) set ) ,{b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) ) : ( ( ) ( non empty finite countable ) Element of bool {b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) : ( ( ) ( finite V35() countable ) set ) ) = {Y : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) ;

for I being ( ( ) ( ) set ) holds Class (nabla I : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total V18(b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) ) reflexive symmetric transitive ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( with_non-empty_elements ) a_partition of b₁ : ( ( ) ( ) set ) ) c= {I : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) ;

for I being ( ( non empty ) ( non empty ) set ) holds Class (nabla I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued total V18(b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) ) reflexive symmetric transitive ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b₁ : ( ( non empty ) ( non empty ) set ) ) = {I : ( ( non empty ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) ;

for I, a being ( ( ) ( ) set ) ex A being ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st {A : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) } : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) = I : ( ( ) ( ) set ) --> {a : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) : ( ( Function-like V18(b₁ : ( ( ) ( ) set ) ,{{b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V35() countable ) set ) ) ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined {{b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V35() countable ) set ) -valued Function-like constant total V18(b₁ : ( ( ) ( ) set ) ,{{b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V35() countable ) set ) ) ) Element of bool [:b₁ : ( ( ) ( ) set ) ,{{b₂ : ( ( ) ( ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V35() countable ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

for I being ( ( ) ( ) set )
for A being ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ex B being ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) c= B : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ;

for I being ( ( ) ( ) set )
for M being ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( V32() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total V32() ) ManySortedSubset of M : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ) ex C being ( ( V2() V32() ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total V32() ) ManySortedSubset of M : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ) st B : ( ( V32() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total V32() ) ManySortedSubset of b₂ : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ) c= C : ( ( V2() V32() ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total V32() ) ManySortedSubset of b₂ : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ) ;

for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F, G being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of A : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ,{B : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) } : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) ) holds F : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b₂ : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ,{b₃ : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) } : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) ) = G : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b₂ : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ,{b₃ : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) } : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) ) ;

for I being ( ( ) ( ) set )
for A being ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of A : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ,{B : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) } : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) ) holds F : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b₂ : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ,{b₃ : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) } : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) ) is "onto" ;

for I being ( ( ) ( ) set )
for A being ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of {A : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) } : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) ,B : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ) holds F : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of {b₂ : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) } : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) ,b₃ : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ) is "1-1" ;

for S being ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign )
for X being ( ( Relation-like V2() the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) holds Reverse X : ( ( Relation-like V2() the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of FreeGen b₂ : ( ( Relation-like V2() the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like V2() non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total free ) GeneratorSet of FreeMSA b₂ : ( ( Relation-like V2() the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( strict non-empty free ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) ,b₂ : ( ( Relation-like V2() the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like V2() non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) ManySortedSet of the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) is "1-1" ;

for I being ( ( ) ( ) set )
for A being ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total V32() ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total V32() ) ManySortedSet of I : ( ( ) ( ) set ) ) ex F being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of I : ( ( ) ( ) set ) --> NAT : ( ( ) ( non empty non trivial V24() V25() V26() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like V18(b₁ : ( ( ) ( ) set ) ,{NAT : ( ( ) ( non empty non trivial V24() V25() V26() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite countable ) set ) ) ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined {NAT : ( ( ) ( non empty non trivial V24() V25() V26() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite countable ) set ) -valued Function-like constant total V18(b₁ : ( ( ) ( ) set ) ,{NAT : ( ( ) ( non empty non trivial V24() V25() V26() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite countable ) set ) ) ) Element of bool [:b₁ : ( ( ) ( ) set ) ,{NAT : ( ( ) ( non empty non trivial V24() V25() V26() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite countable ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ,A : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total V32() ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total V32() ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ) st F : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( ) ( ) set ) --> NAT : ( ( ) ( non empty non trivial V24() V25() V26() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like V18(b₁ : ( ( ) ( ) set ) ,{NAT : ( ( ) ( non empty non trivial V24() V25() V26() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite countable ) set ) ) ) ( Relation-like non-empty b₁ : ( ( ) ( ) set ) -defined {NAT : ( ( ) ( non empty non trivial V24() V25() V26() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite countable ) set ) -valued Function-like constant total V18(b₁ : ( ( ) ( ) set ) ,{NAT : ( ( ) ( non empty non trivial V24() V25() V26() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite countable ) set ) ) ) Element of bool [:b₁ : ( ( ) ( ) set ) ,{NAT : ( ( ) ( non empty non trivial V24() V25() V26() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite countable ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ,b₂ : ( ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total V32() ) ( Relation-like V2() b₁ : ( ( ) ( ) set ) -defined Function-like total V32() ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ) is "onto" ;

for S being ( ( non empty ) ( non empty V54() ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty ) ( non empty V54() ) ManySortedSign ) )
for f, g being ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) -compatible non empty total ) Element of product the Sorts of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) st ( for i being ( ( ) ( ) set ) holds (proj ( the Sorts of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ,i : ( ( ) ( ) set ) )) : ( ( Relation-like Function-like ) ( Relation-like product the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) -defined Function-like non empty total ) set ) . f : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) -compatible non empty total ) Element of product the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) : ( ( ) ( ) set ) = (proj ( the Sorts of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ,i : ( ( ) ( ) set ) )) : ( ( Relation-like Function-like ) ( Relation-like product the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) -defined Function-like non empty total ) set ) . g : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) -compatible non empty total ) Element of product the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) -compatible non empty total ) Element of product the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) = g : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) -compatible non empty total ) Element of product the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty ) ( non empty V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) ;

for S being ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign )
for I being ( ( non empty ) ( non empty ) set )
for s being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of I : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) )
for f, g being ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) -compatible non empty total ) Element of product (Carrier (A : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) st ( for a being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds (proj ((Carrier (A : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) ,a : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) set ) ) )) : ( ( Relation-like Function-like ) ( Relation-like product (Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) -defined Function-like non empty total ) set ) . f : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) -compatible non empty total ) Element of product (Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) : ( ( ) ( ) set ) = (proj ((Carrier (A : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) ,a : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) set ) ) )) : ( ( Relation-like Function-like ) ( Relation-like product (Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) -defined Function-like non empty total ) set ) . g : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) -compatible non empty total ) Element of product (Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) -compatible non empty total ) Element of product (Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) = g : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) -compatible non empty total ) Element of product (Carrier (b₄ : ( ( ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) MSAlgebra-Family of b₂ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,b₃ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) ;

for S being ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign )
for A, B being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) )
for C being ( ( non-empty ) ( non-empty ) MSSubAlgebra of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) )
for h1 being ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) 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 V54() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) st h1 : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) is_homomorphism B : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,C : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) holds
for h2 being ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) 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 V54() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) st h1 : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) = h2 : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) holds
h2 : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) is_homomorphism B : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ;

for S being ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign )
for A, B being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) )
for F being ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) 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 V54() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) st F : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) is_monomorphism A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,B : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) holds
A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) , Image F : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of b₃ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) are_isomorphic ;

for S being ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign )
for A, B being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) )
for F being ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) 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 V54() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) st F : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) is "onto" holds
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( Relation-like Function-like FinSequence-like ) Element of Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,B : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₃ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) ex y being ( ( ) ( Relation-like Function-like FinSequence-like ) Element of Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) st F : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) # y : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of Args (b₅ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of Args (b₅ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₃ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) = x : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of Args (b₅ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₃ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) ;

for S being ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) )
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( Relation-like Function-like FinSequence-like ) Element of Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) holds (Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) )) : ( ( Function-like V18( Args (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) , Result (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty with_non-empty_elements ) set ) ) ) ) ( Relation-like Args (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) -defined Result (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty with_non-empty_elements ) set ) ) -valued Function-like non empty total V18( Args (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) , Result (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty with_non-empty_elements ) set ) ) ) ) Element of bool [:(Args (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) )) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ,(Result (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of rng the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty with_non-empty_elements ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( Relation-like Function-like FinSequence-like ) Element of Args (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng K158( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) : ( ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) ( Relation-like K155( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M8( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like total ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of Result (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty with_non-empty_elements ) set ) ) ) in the Sorts of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) . (the_result_sort_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ;

for S being ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign )
for A, B, C being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) )
for F1 being ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) 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 V54() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) )
for F2 being ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) 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 V54() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) st F1 : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) is_epimorphism A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,B : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) & F2 : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) is_homomorphism A : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,C : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) holds
for G being ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) 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 V54() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) st G : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ** F1 : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the Sorts of b₄ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) = F2 : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) holds
G : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding Relation-yielding ) ManySortedFunction of b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ,b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) is_homomorphism B : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ,C : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V54() ) ManySortedSign ) ) ;