:: MSSUBLAT semantic presentation

begin

theorem :: MSSUBLAT:1
for a being ( ( ) ( ) set ) holds (*--> a : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20(NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,({b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . 0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V33() FinSequence-like FinSubsequence-like ) Element of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) set ) ;

theorem :: MSSUBLAT:2
for a being ( ( ) ( ) set ) holds (*--> a : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20(NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,({b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V33() FinSequence-like FinSubsequence-like ) Element of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) = <*a : ( ( ) ( ) set ) *> : ( ( Relation-like Function-like ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like non empty V33() V40(1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) set ) ;

theorem :: MSSUBLAT:3
for a being ( ( ) ( ) set ) holds (*--> a : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20(NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,({b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . 2 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V33() FinSequence-like FinSubsequence-like ) Element of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) = <*a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like non empty V33() V40(2 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) set ) ;

theorem :: MSSUBLAT:4
for a being ( ( ) ( ) set ) holds (*--> a : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20(NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,({b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . 3 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V33() FinSequence-like FinSubsequence-like ) Element of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) = <*a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like non empty V33() V40(3 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) set ) ;

theorem :: MSSUBLAT:5
for i being ( ( V32() ) ( V26() V27() V28() V32() ) Nat)
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -valued Function-like Function-yielding V25() V33() FinSequence-like FinSubsequence-like ) FinSequence of {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) ) holds
( f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -valued Function-like Function-yielding V25() V33() FinSequence-like FinSubsequence-like ) FinSequence of {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) ) = i : ( ( V32() ) ( V26() V27() V28() V32() ) Nat) |-> 0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V33() V40(b1 : ( ( V32() ) ( V26() V27() V28() V32() ) Nat) ) FinSequence-like FinSubsequence-like ) Element of b1 : ( ( V32() ) ( V26() V27() V28() V32() ) Nat) -tuples_on NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) iff len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -valued Function-like Function-yielding V25() V33() FinSequence-like FinSubsequence-like ) FinSequence of {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) ) : ( ( ) ( V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = i : ( ( V32() ) ( V26() V27() V28() V32() ) Nat) ) ;

theorem :: MSSUBLAT:6
for i being ( ( V32() ) ( V26() V27() V28() V32() ) Nat)
for f being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V33() FinSequence-like FinSubsequence-like ) FinSequence) st f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V33() FinSequence-like FinSubsequence-like ) FinSequence) = (*--> 0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20(NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,({0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . i : ( ( V32() ) ( V26() V27() V28() V32() ) Nat) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V33() FinSequence-like FinSubsequence-like ) set ) holds
len f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V33() FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = i : ( ( V32() ) ( V26() V27() V28() V32() ) Nat) ;

begin

theorem :: MSSUBLAT:7
for U1, U2 being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) st U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) is ( ( ) ( non empty partial quasi_total non-empty ) SubAlgebra of U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) holds
MSSign U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) = MSSign U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ;

theorem :: MSSUBLAT:8
for U1, U2 being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) st U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) is ( ( ) ( non empty partial quasi_total non-empty ) SubAlgebra of U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) holds
for B being ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) st B : ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) = the Sorts of (MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) holds
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) = o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) holds
Den (a : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( Function-like quasi_total ) ( Relation-like Args (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) -defined Result (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) -valued Function-like quasi_total ) Element of K19(K20((Args (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) ,(Result (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) = (Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) )) : ( ( Function-like quasi_total ) ( Relation-like Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng ( the Sorts of (MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) -defined Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) -valued Function-like quasi_total ) Element of K19(K20((Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of rng ( the Sorts of (MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) ,(Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) | (Args (a : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) : ( ( Function-like ) ( Relation-like Args (b5 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng ( the Sorts of (MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) -defined Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng ( the Sorts of (MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) -defined Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) -valued Function-like ) Element of K19(K20((Args (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of rng ( the Sorts of (MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) ,(Result (b4 : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,(MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) )) : ( ( ) ( non empty ) Element of rng the Sorts of (MSAlg b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( ) ( non empty V45() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: MSSUBLAT:9
for U1, U2 being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) st U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) is ( ( ) ( non empty partial quasi_total non-empty ) SubAlgebra of U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) holds
the Sorts of (MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) is ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ;

theorem :: MSSUBLAT:10
for U1, U2 being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) st U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) is ( ( ) ( non empty partial quasi_total non-empty ) SubAlgebra of U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) holds
for B being ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) st B : ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) = the Sorts of (MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) holds
B : ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) is opers_closed ;

theorem :: MSSUBLAT:11
for U1, U2 being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) st U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) is ( ( ) ( non empty partial quasi_total non-empty ) SubAlgebra of U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) holds
for B being ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) st B : ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) = the Sorts of (MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) holds
the Charact of (MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier' of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V25() ) ManySortedFunction of the Arity of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20( the carrier' of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * ( the Sorts of (MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like non-empty non empty-yielding the carrier' of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the ResultSort of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -valued Function-like quasi_total ) Element of K19(K20( the carrier' of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * the Sorts of (MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like non-empty non empty-yielding the carrier' of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) = Opers ((MSAlg U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ,B : ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( ) ( Relation-like the carrier' of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V25() ) ManySortedFunction of the Arity of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20( the carrier' of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * (b3 : ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) #) : ( ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the ResultSort of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -valued Function-like quasi_total ) Element of K19(K20( the carrier' of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * b3 : ( ( ) ( Relation-like the carrier of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) MSSubset of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like ) ( Relation-like the carrier' of (MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) ;

theorem :: MSSUBLAT:12
for U1, U2 being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) st U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) is ( ( ) ( non empty partial quasi_total non-empty ) SubAlgebra of U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) holds
MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of MSAlg U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) ;

theorem :: MSSUBLAT:13
for U1, U2 being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) st MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of MSAlg U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) holds
the carrier of U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) is ( ( ) ( ) Subset of ) ;

theorem :: MSSUBLAT:14
for U1, U2 being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) st MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of MSAlg U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) holds
for B being ( ( non empty ) ( non empty ) Subset of ) st B : ( ( non empty ) ( non empty ) Subset of ) = the carrier of U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) holds
B : ( ( non empty ) ( non empty ) Subset of ) is opers_closed ;

theorem :: MSSUBLAT:15
for U1, U2 being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) st MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of MSAlg U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) holds
for B being ( ( non empty ) ( non empty ) Subset of ) st B : ( ( non empty ) ( non empty ) Subset of ) = the carrier of U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) holds
the charact of U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( Relation-like non-empty NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs (( the carrier of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total ) FinSequence of PFuncs (( the carrier of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = Opers (U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ,B : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs ((b3 : ( ( non empty ) ( non empty ) Subset of ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b3 : ( ( non empty ) ( non empty ) Subset of ) ) ,b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( ) set ) -valued Function-like V33() FinSequence-like FinSubsequence-like ) FinSequence of PFuncs ((b3 : ( ( non empty ) ( non empty ) Subset of ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b3 : ( ( non empty ) ( non empty ) Subset of ) ) ,b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( ) set ) ) ;

theorem :: MSSUBLAT:16
for U1, U2 being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) st MSAlg U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of MSAlg U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) holds
U1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) is ( ( ) ( non empty partial quasi_total non-empty ) SubAlgebra of U2 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) ;

theorem :: MSSUBLAT:17
for MS being ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) )
for B being ( ( non-empty ) ( non-empty ) MSSubAlgebra of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) holds the carrier of (1-Alg B : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( ) ( non empty ) set ) is ( ( ) ( ) Subset of ) ;

theorem :: MSSUBLAT:18
for MS being ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) )
for B being ( ( non-empty ) ( non-empty ) MSSubAlgebra of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) )
for S being ( ( non empty ) ( non empty ) Subset of ) st S : ( ( non empty ) ( non empty ) Subset of ) = the carrier of (1-Alg B : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( ) ( non empty ) set ) holds
S : ( ( non empty ) ( non empty ) Subset of ) is opers_closed ;

theorem :: MSSUBLAT:19
for MS being ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) )
for B being ( ( non-empty ) ( non-empty ) MSSubAlgebra of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) )
for S being ( ( non empty ) ( non empty ) Subset of ) st S : ( ( non empty ) ( non empty ) Subset of ) = the carrier of (1-Alg B : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( ) ( non empty ) set ) holds
the charact of (1-Alg B : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( ) ( Relation-like non-empty NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs (( the carrier of (1-Alg b3 : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (1-Alg b3 : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( ) ( non empty ) set ) ) , the carrier of (1-Alg b3 : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total ) FinSequence of PFuncs (( the carrier of (1-Alg b3 : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (1-Alg b3 : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( ) ( non empty ) set ) ) , the carrier of (1-Alg b3 : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = Opers ((1-Alg A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) ,S : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs ((b4 : ( ( non empty ) ( non empty ) Subset of ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b4 : ( ( non empty ) ( non empty ) Subset of ) ) ,b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( ) set ) -valued Function-like V33() FinSequence-like FinSubsequence-like ) FinSequence of PFuncs ((b4 : ( ( non empty ) ( non empty ) Subset of ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of b4 : ( ( non empty ) ( non empty ) Subset of ) ) ,b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( ) set ) ) ;

theorem :: MSSUBLAT:20
for MS being ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) )
for B being ( ( non-empty ) ( non-empty ) MSSubAlgebra of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) holds 1-Alg B : ( ( non-empty ) ( non-empty ) MSSubAlgebra of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) is ( ( ) ( non empty partial quasi_total non-empty ) SubAlgebra of 1-Alg A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) ) ;

theorem :: MSSUBLAT:21
for S being ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign )
for A, B being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) ) holds
( A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of B : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) ) ) iff A : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of MSAlgebra(# the Sorts of B : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the Charact of B : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier' of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V25() ) ManySortedFunction of the Arity of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20( the carrier' of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * ( the Sorts of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the ResultSort of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of K19(K20( the carrier' of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * the Sorts of b3 : ( ( ) ( ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V70() ) ManySortedSign ) ) ) ) ;

theorem :: MSSUBLAT:22
for A, B being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) holds
( signature A : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V33() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = signature B : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V33() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff MSSign A : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) = MSSign B : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ;

theorem :: MSSUBLAT:23
for MS being ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) st the carrier of MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) = {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) holds
MSSign (1-Alg A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) = ManySortedSign(# the carrier of MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) , the carrier' of MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the Arity of MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20( the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) , the ResultSort of MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -valued Function-like quasi_total ) Element of K19(K20( the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty V70() strict ) ManySortedSign ) ;

theorem :: MSSUBLAT:24
for MS being ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign )
for A, B being ( ( non-empty ) ( non-empty ) MSAlgebra over MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) st 1-Alg A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) = 1-Alg B : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) holds
MSAlgebra(# the Sorts of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) , the Charact of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V25() ) ManySortedFunction of the Arity of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20( the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * ( the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like non-empty non empty-yielding the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the ResultSort of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -valued Function-like quasi_total ) Element of K19(K20( the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like non-empty non empty-yielding the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) #) : ( ( strict ) ( strict non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) = MSAlgebra(# the Sorts of B : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) , the Charact of B : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V25() ) ManySortedFunction of the Arity of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20( the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * ( the Sorts of b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the ResultSort of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -valued Function-like quasi_total ) Element of K19(K20( the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * the Sorts of b3 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) #) : ( ( strict ) ( strict non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ;

theorem :: MSSUBLAT:25
for MS being ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) st the carrier of MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) = {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) holds
the Sorts of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) = the Sorts of (MSAlg (1-Alg A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign (1-Alg b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of (MSSign (1-Alg b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign (1-Alg b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) ;

theorem :: MSSUBLAT:26
for MS being ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign )
for A being ( ( non-empty ) ( non-empty ) MSAlgebra over MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) st the carrier of MS : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) = {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) holds
MSAlg (1-Alg A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign (1-Alg b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) = MSAlgebra(# the Sorts of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) , the Charact of A : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total Function-yielding V25() ) ManySortedFunction of the Arity of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -valued Function-like quasi_total Function-yielding V25() ) Element of K19(K20( the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * ( the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) #) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like non-empty non empty-yielding the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) , the ResultSort of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -valued Function-like quasi_total ) Element of K19(K20( the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( Relation-like ) ( Relation-like non-empty non empty-yielding the carrier' of b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty total ) set ) ) #) : ( ( strict ) ( strict non-empty ) MSAlgebra over b1 : ( ( non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() segmental ) ManySortedSign ) ) ;

theorem :: MSSUBLAT:27
for A being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra)
for B being ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg A : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) st the carrier of (MSSign A : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) = {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) holds
1-Alg B : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) UAStr ) is ( ( ) ( non empty partial quasi_total non-empty ) SubAlgebra of A : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) ;

begin

theorem :: MSSUBLAT:28
for A being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra)
for a1, b1 being ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of A : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) )
for a2, b2 being ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg A : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) st a2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) = MSAlg a1 : ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) & b2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) = MSAlg b1 : ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b3 : ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) holds
the Sorts of a2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) \/ the Sorts of b2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) = 0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) .--> ( the carrier of a1 : ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( ) ( non empty ) set ) \/ the carrier of b1 : ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( Relation-like {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -defined NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -defined Function-like one-to-one ) set ) ;

theorem :: MSSUBLAT:29
for A being ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra)
for a1, b1 being ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of A : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) )
for a2, b2 being ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg A : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) st a2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) = MSAlg a1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) & b2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) = MSAlg b1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b3 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) holds
the Sorts of a2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) /\ the Sorts of b2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like non-empty non empty-yielding the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) : ( ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like total ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V33() ) set ) -defined Function-like non empty total ) set ) = 0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) .--> ( the carrier of a1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( ) ( non empty ) set ) /\ the carrier of b1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty ) ( non empty partial quasi_total non-empty ) Universal_Algebra) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( Relation-like {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -defined NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined {0 : ( ( ) ( Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty ) set ) -defined Function-like one-to-one ) set ) ;

theorem :: MSSUBLAT:30
for A being ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra)
for a1, b1 being ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of A : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) )
for a2, b2 being ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg A : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) st a2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) = MSAlg a1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) & b2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) = MSAlg b1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b3 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) holds
MSAlg (a1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) ) "\/" b1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) ) ) : ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign (b2 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) ) "\/" b3 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) ) ) : ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) = a2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) "\/" b2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) : ( ( strict ) ( strict ) MSSubAlgebra of MSAlg b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty strict partial quasi_total non-empty ) ( non empty strict partial quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) ) ;

registration
let A be ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ;
cluster MSSign A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) UAStr ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) -> trivial non void strict segmental all-with_const_op ;
end;

theorem :: MSSUBLAT:31
for A being ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra)
for a1, b1 being ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) )
for a2, b2 being ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental all-with_const_op ) ManySortedSign ) ) ) st a2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental all-with_const_op ) ManySortedSign ) ) ) = MSAlg a1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b2 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) & b2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental all-with_const_op ) ManySortedSign ) ) ) = MSAlg b1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b3 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) holds
MSAlg (a1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ) /\ b1 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ) ) : ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign (b2 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ) /\ b3 : ( ( strict non-empty ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ) ) : ( ( strict ) ( non empty strict partial quasi_total non-empty ) SubAlgebra of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental ) ManySortedSign ) ) = a2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental all-with_const_op ) ManySortedSign ) ) ) /\ b2 : ( ( strict non-empty ) ( strict non-empty ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental all-with_const_op ) ManySortedSign ) ) ) : ( ( strict ) ( strict ) MSSubAlgebra of MSAlg b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental all-with_const_op ) ManySortedSign ) ) ) ;

registration
let A be ( ( quasi_total ) ( quasi_total ) UAStr ) ;
cluster UAStr(# the carrier of A : ( ( quasi_total ) ( quasi_total ) UAStr ) : ( ( ) ( ) set ) , the charact of A : ( ( quasi_total ) ( quasi_total ) UAStr ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs (( the carrier of A : ( ( quasi_total ) ( quasi_total ) UAStr ) : ( ( ) ( ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of A : ( ( quasi_total ) ( quasi_total ) UAStr ) : ( ( ) ( ) set ) ) , the carrier of A : ( ( quasi_total ) ( quasi_total ) UAStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like V33() FinSequence-like FinSubsequence-like quasi_total ) FinSequence of PFuncs (( the carrier of A : ( ( quasi_total ) ( quasi_total ) UAStr ) : ( ( ) ( ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of A : ( ( quasi_total ) ( quasi_total ) UAStr ) : ( ( ) ( ) set ) ) , the carrier of A : ( ( quasi_total ) ( quasi_total ) UAStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) UAStr ) -> strict quasi_total ;
end;

registration
let A be ( ( partial ) ( partial ) UAStr ) ;
cluster UAStr(# the carrier of A : ( ( partial ) ( partial ) UAStr ) : ( ( ) ( ) set ) , the charact of A : ( ( partial ) ( partial ) UAStr ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs (( the carrier of A : ( ( partial ) ( partial ) UAStr ) : ( ( ) ( ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of A : ( ( partial ) ( partial ) UAStr ) : ( ( ) ( ) set ) ) , the carrier of A : ( ( partial ) ( partial ) UAStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like V33() FinSequence-like FinSubsequence-like homogeneous ) FinSequence of PFuncs (( the carrier of A : ( ( partial ) ( partial ) UAStr ) : ( ( ) ( ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of A : ( ( partial ) ( partial ) UAStr ) : ( ( ) ( ) set ) ) , the carrier of A : ( ( partial ) ( partial ) UAStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) UAStr ) -> strict partial ;
end;

registration
let A be ( ( non-empty ) ( non-empty ) UAStr ) ;
cluster UAStr(# the carrier of A : ( ( non-empty ) ( non-empty ) UAStr ) : ( ( ) ( ) set ) , the charact of A : ( ( non-empty ) ( non-empty ) UAStr ) : ( ( ) ( Relation-like non-empty NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs (( the carrier of A : ( ( non-empty ) ( non-empty ) UAStr ) : ( ( ) ( ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of A : ( ( non-empty ) ( non-empty ) UAStr ) : ( ( ) ( ) set ) ) , the carrier of A : ( ( non-empty ) ( non-empty ) UAStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like ) FinSequence of PFuncs (( the carrier of A : ( ( non-empty ) ( non-empty ) UAStr ) : ( ( ) ( ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of A : ( ( non-empty ) ( non-empty ) UAStr ) : ( ( ) ( ) set ) ) , the carrier of A : ( ( non-empty ) ( non-empty ) UAStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) UAStr ) -> strict non-empty ;
end;

registration
let A be ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) ;
cluster UAStr(# the carrier of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) UAStr ) : ( ( ) ( non empty ) set ) , the charact of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) UAStr ) : ( ( ) ( Relation-like non-empty NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs (( the carrier of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) UAStr ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) UAStr ) : ( ( ) ( non empty ) set ) ) , the carrier of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) UAStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total ) FinSequence of PFuncs (( the carrier of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) UAStr ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) UAStr ) : ( ( ) ( non empty ) set ) ) , the carrier of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) UAStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict partial quasi_total non-empty ) UAStr ) -> strict with_const_op ;
end;

theorem :: MSSUBLAT:32
for A being ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) holds UnSubAlLattice UAStr(# the carrier of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the charact of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( Relation-like non-empty NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs (( the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total ) FinSequence of PFuncs (( the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict partial quasi_total non-empty with_const_op ) UAStr ) : ( ( non empty strict Lattice-like ) ( non empty strict Lattice-like ) LattStr ) , MSSubAlLattice (MSAlg UAStr(# the carrier of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the charact of A : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( Relation-like non-empty NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs (( the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total ) FinSequence of PFuncs (( the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict partial quasi_total non-empty with_const_op ) UAStr ) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign UAStr(# the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the charact of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( Relation-like non-empty NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined PFuncs (( the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total ) FinSequence of PFuncs (( the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) *) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty partial quasi_total non-empty with_const_op ) ( non empty partial quasi_total non-empty with_const_op ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict partial quasi_total non-empty with_const_op ) UAStr ) : ( ( trivial non void strict segmental ) ( non empty trivial V64() non void 1 : ( ( ) ( non empty V26() V27() V28() V32() ) Element of NAT : ( ( ) ( non empty V26() V27() V28() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element V70() strict segmental all-with_const_op ) ManySortedSign ) ) : ( ( non empty strict Lattice-like ) ( non empty strict Lattice-like V86() ) LattStr ) are_isomorphic ;