:: MSUHOM_1 semantic presentation

begin

theorem :: MSUHOM_1:1
for f, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for C being ( ( ) ( ) set ) st rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= C : ( ( ) ( ) set ) holds
(g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) | C : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) * f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like ) ( Relation-like Function-like ) set ) = g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) * f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like ) ( Relation-like Function-like ) set ) ;

theorem :: MSUHOM_1:2
for I being ( ( ) ( ) set )
for C being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds C : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) c= I : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b1 : ( ( ) ( ) set ) ) ;

theorem :: MSUHOM_1:3
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for C being ( ( ) ( ) set ) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is Function-yielding holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) | C : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) is Function-yielding ;

theorem :: MSUHOM_1:4
for I being ( ( ) ( ) set )
for C being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds (M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) | C : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Relation-like ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) # : ( ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) -defined Function-like non empty total ) set ) = (M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) #) : ( ( Relation-like b1 : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b1 : ( ( ) ( ) set ) ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b1 : ( ( ) ( ) set ) ) -defined Function-like non empty total ) set ) | (C : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Relation-like ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) -defined b1 : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b1 : ( ( ) ( ) set ) ) -defined Function-like ) set ) ;

definition
let S, S9 be ( ( non empty ) ( non empty V67() ) ManySortedSign ) ;
pred S <= S9 means :: MSUHOM_1:def 1
( the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) c= the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) & the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) c= the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) & the Arity of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( Function-like V18( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) -valued Function-like total V18( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ,( the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) | the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) -valued Function-like Function-yielding V22() ) Element of K19(K20( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ,( the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) = the Arity of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) & the ResultSort of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( Function-like V18( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) | the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -valued Function-like ) Element of K19(K20( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) = the ResultSort of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) );
reflexivity
for S being ( ( non empty ) ( non empty V67() ) ManySortedSign ) holds
( the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) c= the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) & the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) c= the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) & the Arity of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like total V18( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) ,( the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) | the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like Function-yielding V22() ) Element of K19(K20( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) ,( the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) = the Arity of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like total V18( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) ,( the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) & the ResultSort of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like total V18( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) | the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K19(K20( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) = the ResultSort of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like total V18( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier' of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

theorem :: MSUHOM_1:5
for S, S9, S99 being ( ( non empty ) ( non empty V67() ) ManySortedSign ) st S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) <= S9 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) & S9 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) <= S99 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) holds
S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) <= S99 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ;

theorem :: MSUHOM_1:6
for S, S9 being ( ( non empty strict ) ( non empty V67() strict ) ManySortedSign ) st S : ( ( non empty strict ) ( non empty V67() strict ) ManySortedSign ) <= S9 : ( ( non empty strict ) ( non empty V67() strict ) ManySortedSign ) & S9 : ( ( non empty strict ) ( non empty V67() strict ) ManySortedSign ) <= S : ( ( non empty strict ) ( non empty V67() strict ) ManySortedSign ) holds
S : ( ( non empty strict ) ( non empty V67() strict ) ManySortedSign ) = S9 : ( ( non empty strict ) ( non empty V67() strict ) ManySortedSign ) ;

theorem :: MSUHOM_1:7
for n being ( ( V29() ) ( V23() V24() V25() V29() V119() V120() ext-real ) Nat)
for A being ( ( non empty ) ( non empty ) set )
for g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for a being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) )
for k being ( ( V29() ) ( V23() V24() V25() V29() V119() V120() ext-real ) Nat) st 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( V29() ) ( V23() V24() V25() V29() V119() V120() ext-real ) Nat) & k : ( ( V29() ) ( V23() V24() V25() V29() V119() V120() ext-real ) Nat) <= n : ( ( V29() ) ( V23() V24() V25() V29() V119() V120() ext-real ) Nat) holds
(a : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) .--> g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {b4 : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) -defined Function-like one-to-one Function-yielding V22() ) set ) . ((n : ( ( V29() ) ( V23() V24() V25() V29() V119() V120() ext-real ) Nat) |-> a : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V30() FinSequence-like FinSubsequence-like ) Element of b1 : ( ( V29() ) ( V23() V24() V25() V29() V119() V120() ext-real ) Nat) -tuples_on b2 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) FinSequenceSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) /. k : ( ( V29() ) ( V23() V24() V25() V29() V119() V120() ext-real ) Nat) ) : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) = g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;

theorem :: MSUHOM_1:8
for I being ( ( ) ( ) set )
for I0 being ( ( ) ( ) Subset of ( ( ) ( ) 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 V22() ) 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 A0, B0 being ( ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total ) ManySortedSet of I0 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) st A0 : ( ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) = A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) | I0 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) & B0 : ( ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) = B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) | I0 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) holds
F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V22() ) ManySortedFunction of b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) | I0 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V22() ) set ) is ( ( ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total Function-yielding V22() ) ManySortedFunction of A0 : ( ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) ,B0 : ( ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) ) ;

definition
let S, S9 be ( ( non empty non void strict ) ( non empty non void V67() strict ) ManySortedSign ) ;
let A be ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over S9 : ( ( non empty non void strict ) ( non empty non void V67() strict ) ManySortedSign ) ) ;
assume S : ( ( non empty non void strict ) ( non empty non void V67() strict ) ManySortedSign ) <= S9 : ( ( non empty non void strict ) ( non empty non void V67() strict ) ManySortedSign ) ;
func A Over S -> ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) means :: MSUHOM_1:def 2
( the Sorts of it : ( ( Function-like V18(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ) ( Relation-like S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) -defined S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) -valued Function-like V18(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ) Element of K19(K20(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) = the Sorts of A : ( ( ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V22() ) ManySortedFunction of the Arity of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * (S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) #) : ( ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total ) set ) , the ResultSort of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( Relation-like ) ( Relation-like ) set ) ) : ( ( Relation-like the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like total ) set ) | the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) : ( ( Relation-like ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like ) set ) & the Charact of it : ( ( Function-like V18(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ) ( Relation-like S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) -defined S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) -valued Function-like V18(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ) Element of K19(K20(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V22() ) ManySortedFunction of the Arity of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * ( the Sorts of it : ( ( Function-like V18(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ) ( Relation-like S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) -defined S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) -valued Function-like V18(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ) Element of K19(K20(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total ) set ) , the ResultSort of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * the Sorts of it : ( ( Function-like V18(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ) ( Relation-like S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) -defined S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) -valued Function-like V18(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ) Element of K19(K20(S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) ,S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) = the Charact of A : ( ( ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V22() ) ManySortedFunction of the Arity of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * (S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) #) : ( ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total ) set ) , the ResultSort of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( Relation-like ) ( Relation-like ) set ) ) : ( ( ) ( Relation-like the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V22() ) ManySortedFunction of the Arity of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( Function-like V18( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) -valued Function-like total V18( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ,( the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * ( the Sorts of A : ( ( ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V22() ) ManySortedFunction of the Arity of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * (S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) #) : ( ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total ) set ) , the ResultSort of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( Relation-like ) ( Relation-like ) set ) ) : ( ( Relation-like the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like total ) set ) #) : ( ( Relation-like the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) -defined Function-like total ) ( Relation-like the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like total ) set ) , the ResultSort of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( Function-like V18( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) , the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * the Sorts of A : ( ( ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V22() ) ManySortedFunction of the Arity of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * (S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) #) : ( ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total ) set ) , the ResultSort of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like total V18( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( Relation-like ) ( Relation-like ) set ) ) : ( ( Relation-like the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like ) set ) ) | the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier' of S9 : ( ( ) ( ) MSAlgebra over S : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( ) ( ) set ) -defined Function-like Function-yielding V22() ) set ) );
end;

theorem :: MSUHOM_1:9
for S being ( ( non empty non void strict ) ( non empty non void V67() strict ) ManySortedSign )
for A being ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over S : ( ( non empty non void strict ) ( non empty non void V67() strict ) ManySortedSign ) ) holds A : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void strict ) ( non empty non void V67() strict ) ManySortedSign ) ) = A : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void strict ) ( non empty non void V67() strict ) ManySortedSign ) ) Over S : ( ( non empty non void strict ) ( non empty non void V67() strict ) ManySortedSign ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over b1 : ( ( non empty non void strict ) ( non empty non void V67() strict ) ManySortedSign ) ) ;

theorem :: MSUHOM_1:10
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) st U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) are_similar holds
MSSign U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) = MSSign U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ;

definition
let U1, U2 be ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ;
let h be ( ( Function-like V18( the carrier of U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
assume MSSign U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) = MSSign U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ;
func MSAlg h -> ( ( ) ( Relation-like the carrier of (MSSign U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( V60() non void strict segmental ) ( V60() V61() non void strict segmental ) ManySortedSign ) : ( ( ) ( V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( V60() non void strict segmental ) ( V60() V61() non void strict segmental ) ManySortedSign ) ,(MSSign U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( V60() non void strict segmental ) ( V60() V61() non void strict segmental ) ManySortedSign ) ) equals :: MSUHOM_1:def 3
0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() V30() FinSequence-like FinSubsequence-like FinSequence-membered V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) .--> h : ( ( ) ( Relation-like the carrier' of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V22() ) ManySortedFunction of the Arity of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like the carrier' of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like total V18( the carrier' of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Function-yielding V22() ) Element of K19(K20( the carrier' of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) ,( the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * (U2 : ( ( ) ( ) MSAlgebra over U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) #) : ( ( Relation-like the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined Function-like total ) set ) , the ResultSort of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( Function-like V18( the carrier' of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier' of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) -defined the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like total V18( the carrier' of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier' of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( ) set ) , the carrier of U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * U2 : ( ( ) ( ) MSAlgebra over U1 : ( ( non empty ) ( non empty V67() ) ManySortedSign ) ) : ( ( Relation-like ) ( Relation-like ) set ) ) : ( ( ) ( Relation-like {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() V30() FinSequence-like FinSubsequence-like FinSequence-membered V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -defined NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() V30() FinSequence-like FinSubsequence-like FinSequence-membered V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -defined Function-like one-to-one Function-yielding V22() ) set ) ;
end;

theorem :: MSUHOM_1:11
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) are_similar holds
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) holds (MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) . (the_result_sort_of o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) : ( ( Function-like V18( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) . (the_result_sort_of b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) : ( ( ) ( non empty ) set ) , the Sorts of ((MSAlg b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) . (the_result_sort_of b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) . (the_result_sort_of b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) : ( ( ) ( non empty ) set ) -defined the Sorts of ((MSAlg b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) . (the_result_sort_of b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) . (the_result_sort_of b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) : ( ( ) ( non empty ) set ) , the Sorts of ((MSAlg b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) . (the_result_sort_of b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20(( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) . (the_result_sort_of b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) ) : ( ( ) ( non empty ) set ) ,( the Sorts of ((MSAlg b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) . (the_result_sort_of b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) = h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

theorem :: MSUHOM_1:12
for U1 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) holds Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( Function-like V18( Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) , Result (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V42() ) set ) ) ) ) ( Relation-like Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V42() ) set ) ) -valued Function-like non empty total V18( Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) , Result (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V42() ) set ) ) ) ) Element of K19(K20((Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V42() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) = the charact of U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs (( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V30() FinSequence-like FinSubsequence-like ) FinSequence of PFuncs (( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) . o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ;

theorem :: MSUHOM_1:13
for U1 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) holds Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( Function-like V18( Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) , Result (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V42() ) set ) ) ) ) ( Relation-like Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V42() ) set ) ) -valued Function-like non empty total V18( Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) , Result (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V42() ) set ) ) ) ) Element of K19(K20((Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V42() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) is ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V101() V102( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) operation of ( ( ) ( non empty ) M15( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) )) ) ;

theorem :: MSUHOM_1:14
for U1 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( Relation-like Function-like ) Element of Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) holds y : ( ( ) ( Relation-like Function-like ) Element of Args (b2 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) is ( ( ) ( Relation-like NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like V30() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: MSUHOM_1:15
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) are_similar holds
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( Relation-like Function-like ) Element of Args (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) holds (MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) # y : ( ( ) ( Relation-like Function-like ) Element of Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like ) Element of Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,((MSAlg b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of ((MSAlg b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) = h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * y : ( ( ) ( Relation-like Function-like ) Element of Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( functional non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like ) set ) ;

theorem :: MSUHOM_1:16
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_homomorphism U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) holds
MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) is_homomorphism MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ,(MSAlg U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ;

theorem :: MSUHOM_1:17
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) are_similar holds
MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) is ( ( Relation-like {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() V30() FinSequence-like FinSubsequence-like FinSequence-membered V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -defined Function-like total ) ( Relation-like {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() V30() FinSequence-like FinSubsequence-like FinSequence-membered V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -defined Function-like non empty total ) ManySortedSet of {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() V30() FinSequence-like FinSubsequence-like FinSequence-membered V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) ) ;

theorem :: MSUHOM_1:18
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_epimorphism U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) holds
MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) is_epimorphism MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ,(MSAlg U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ;

theorem :: MSUHOM_1:19
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_monomorphism U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) holds
MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) is_monomorphism MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ,(MSAlg U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ;

theorem :: MSUHOM_1:20
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_isomorphism U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) holds
MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) is_isomorphism MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ,(MSAlg U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ;

theorem :: MSUHOM_1:21
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) are_similar & MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) is_homomorphism MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ,(MSAlg U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) holds
h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_homomorphism U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ;

theorem :: MSUHOM_1:22
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) are_similar & MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) is_epimorphism MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ,(MSAlg U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) holds
h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_epimorphism U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ;

theorem :: MSUHOM_1:23
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) are_similar & MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) is_monomorphism MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ,(MSAlg U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) holds
h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_monomorphism U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ;

theorem :: MSUHOM_1:24
for U1, U2 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra)
for h being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) are_similar & MSAlg h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) is_isomorphism MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ,(MSAlg U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) Over (MSSign U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( strict non-empty ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) holds
h : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_isomorphism U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ;

theorem :: MSUHOM_1:25
for U1 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) holds MSAlg (id the carrier of U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( total ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) = id the Sorts of (MSAlg U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) , the Sorts of (MSAlg b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total ) set ) ) ;

theorem :: MSUHOM_1:26
for U1, U2, U3 being ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) st U1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) are_similar & U2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ,U3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) are_similar holds
for h1 being ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for h2 being ( ( Function-like V18( the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds (MSAlg h2 : ( ( Function-like V18( the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ** (MSAlg h1 : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like Function-yielding V22() ) set ) = MSAlg (h2 : ( ( Function-like V18( the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * h1 : ( ( Function-like V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty total V18( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier of b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) : ( ( ) ( non empty V12() V30() ) set ) -defined Function-like non empty total Function-yielding V22() ) ManySortedFunction of (MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V91() V92() non-empty ) ( non empty V91() V92() non-empty ) Universal_Algebra) ) : ( ( V60() non void strict segmental ) ( non empty V60() V61() non void 1 : ( ( ) ( non empty V23() V24() V25() V29() V119() V120() ext-real ) Element of NAT : ( ( ) ( non empty V23() V24() V25() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V67() strict segmental ) ManySortedSign ) ) ;