MSUALG

definition

let S be ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ;
let U0 be ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;
let s be ( ( ) ( ) SortSymbol of ( ( ) ( non empty ) set ) ) ;

func Constants (U0,s) -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) means :: MSUALG_2:def 3
ex A being ( ( non empty ) ( non empty ) set ) st
( A : ( ( non empty ) ( non empty ) set ) = the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) . s : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12(S : ( ( ) ( ) set ) )) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,(S : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12(S : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) & it : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = { a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) where a is ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) : ex o being ( ( ) ( ) OperSymbol of ( ( ) ( ) set ) ) st
( the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like K168() : ( ( ) ( ) Element of bool K164() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like V34() FinSequence-like FinSubsequence-like ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding K168() : ( ( ) ( ) Element of bool K164() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ) set ) & the ResultSort of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = s : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12(S : ( ( ) ( ) set ) )) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,(S : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12(S : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) in rng (Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like Args (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,U0 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of rng ( the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,U0 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of rng the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) : ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of bool [:(Args (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( ) ( ) Element of rng ( the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b₃ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( ) ( ) Element of rng the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) } ) if the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) . s : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12(S : ( ( ) ( ) set ) )) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,(S : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12(S : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding K168() : ( ( ) ( ) Element of bool K164() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ) set )
otherwise it : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding K168() : ( ( ) ( ) Element of bool K164() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ) set ) ;

end;

definition

pred A is_closed_on o means :: MSUALG_2:def 5
rng ((Den (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like Args (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of rng ( the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of rng the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) : ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of bool [:(Args (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( ) ( ) Element of rng ( the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( ) ( ) Element of rng the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) | (((A : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) * the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) . o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ((A : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) * the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) . o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Args (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of rng ( the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of rng the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) : ( ( ) ( ) set ) ) -valued Function-like ) set ) : ( ( ) ( ) set ) c= (A : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the ResultSort of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like ) set ) . o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;

end;

theorem :: MSUALG_2:2

definition

let S be ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ;
let U0 be ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;
let o be ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ;
let A be ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ;
assume A : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) is_closed_on o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ;

func o /. A -> ( ( Function-like quasi_total ) ( Relation-like ((A : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) * the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) . o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined (A : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the ResultSort of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like ) set ) . o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ((A : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) * the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) . o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(A : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the ResultSort of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like ) set ) . o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) equals :: MSUALG_2:def 7
(Den (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like Args (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of rng ( the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of rng the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) : ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of bool [:(Args (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( ) ( ) Element of rng ( the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) )) : ( ( ) ( ) Element of rng the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) | (((A : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) * the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) . o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ((A : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) * the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) . o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Args (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of rng ( the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (o : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,U0 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of rng the Sorts of U0 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) : ( ( ) ( ) set ) ) -valued Function-like ) set ) ;

end;

definition

func Opers (U0,A) -> ( ( ) ( non empty Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V83() ) ManySortedFunction of (A : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) * the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) ,A : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * the ResultSort of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like ) set ) ) means :: MSUALG_2:def 8
for o being ( ( ) ( ) OperSymbol of ( ( ) ( ) set ) ) holds it : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( ) ( ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like V17(U0 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:U0 : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) /. A : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like ((A : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) * the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) . b₁ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined (A : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * the ResultSort of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like ) set ) . b₁ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ((A : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) * the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) . b₁ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,(A : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * the ResultSort of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like ) set ) . b₁ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

end;

theorem :: MSUALG_2:3

for S being ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign )
for U0 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) )
for B being ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) st B : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) = the Sorts of U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) holds
( B : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) is opers_closed & ( for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) holds o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) /. B : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Function-like quasi_total ) ( Relation-like ((b₃ : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) . b₄ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined (b₃ : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) * the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) . b₄ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ((b₃ : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) . b₄ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ,(b₃ : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) * the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) . b₄ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Function-like quasi_total ) ( Relation-like Args (b₄ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b₄ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng the Sorts of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Element of bool [:(Args (b₄ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) )) : ( ( ) ( ) Element of rng ( the Sorts of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b₄ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) )) : ( ( ) ( ) Element of rng the Sorts of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: MSUALG_2:4

definition

let S be ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ;
let U0 be ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;

mode MSSubAlgebra of U0 -> ( ( ) ( ) MSAlgebra over S : ( ( ) ( ) set ) ) means :: MSUALG_2:def 9
( the Sorts of it : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) is ( ( ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) MSSubset of U0 : ( ( ) ( ) set ) ) & ( for B being ( ( ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) MSSubset of U0 : ( ( ) ( ) set ) ) st B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) = the Sorts of it : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) holds
( B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) is opers_closed & the Charact of it : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V83() ) ManySortedFunction of the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of it : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) , the ResultSort of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of it : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like ) set ) ) = Opers (U0 : ( ( ) ( ) set ) ,B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) : ( ( ) ( non empty Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V83() ) ManySortedFunction of (b₁ : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) #) : ( ( Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined Function-like V17( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) set ) * the Arity of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like V17( the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) set ) ,b₁ : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) * the ResultSort of S : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined Function-like ) set ) ) ) ) );

end;

registration

cluster MSAlgebra(# the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like non-empty non empty-yielding the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) -> strict non-empty ;

end;

theorem :: MSUALG_2:5

for S being ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign )
for U0, U1 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) st MSAlgebra(# the Sorts of U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) = MSAlgebra(# the Sorts of U1 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U1 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) holds
U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of U1 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ;

theorem :: MSUALG_2:7

for S being ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign )
for U1, U2 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) st U1 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of U2 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) & U2 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of U1 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) holds
MSAlgebra(# the Sorts of U1 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U1 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) = MSAlgebra(# the Sorts of U2 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U2 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;

theorem :: MSUALG_2:9

for S being ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign )
for U0 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) )
for U1, U2 being ( ( ) ( ) MSSubAlgebra of U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) st the Sorts of U1 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) = the Sorts of U2 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) holds
MSAlgebra(# the Sorts of U1 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U1 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b₃ : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b₃ : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) = MSAlgebra(# the Sorts of U2 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U2 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b₄ : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b₄ : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;

definition

func SubSort A -> ( ( ) ( ) set ) means :: MSUALG_2:def 10
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( Function-like quasi_total ) ( Relation-like U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) -defined S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) -valued Function-like V17(U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) quasi_total ) Element of bool [:U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ,S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) iff ( x : ( ( ) ( ) set ) in Funcs ( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,(bool (Union the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (Union the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , bool (Union the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool (Union the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & x : ( ( ) ( ) set ) is ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) & ( for B being ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) st B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) = x : ( ( ) ( ) set ) holds
( B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) is opers_closed & Constants U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) c= B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) & A : ( ( ) ( ) Element of the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) ) ) );

end;

definition

let S be ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ;
let U0 be ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;

func SubSort U0 -> ( ( ) ( ) set ) means :: MSUALG_2:def 11
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) iff ( x : ( ( ) ( ) set ) in Funcs ( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,(bool (Union the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (Union the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , bool (Union the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool (Union the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & x : ( ( ) ( ) set ) is ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) & ( for B being ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) st B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) = x : ( ( ) ( ) set ) holds
B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) is opers_closed ) ) );

end;

theorem :: MSUALG_2:17

theorem :: MSUALG_2:18

for S being ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign )
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for U0 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) )
for A, B being ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) st B : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) in SubSort A : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) set ) holds
rng ((Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) )) : ( ( Function-like quasi_total ) ( Relation-like Args (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Element of bool [:(Args (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) )) : ( ( ) ( ) Element of rng ( the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) )) : ( ( ) ( ) Element of rng the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) | ((((MSSubSort A : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) . o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like (((MSSubSort b₄ : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) . b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined Args (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like ) set ) : ( ( ) ( ) set ) c= (B : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) * the ResultSort of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) . o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ;

theorem :: MSUALG_2:19

for S being ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign )
for o being ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) )
for U0 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) )
for A being ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) holds rng ((Den (o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) )) : ( ( Function-like quasi_total ) ( Relation-like Args (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Element of bool [:(Args (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) )) : ( ( ) ( ) Element of rng ( the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) ,(Result (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) )) : ( ( ) ( ) Element of rng the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) | ((((MSSubSort A : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) . o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like (((MSSubSort b₄ : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) . b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined Args (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng ( the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( ) ( non empty ) set ) ) -defined Result (b₂ : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( ) Element of rng the Sorts of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like ) set ) : ( ( ) ( ) set ) c= ((MSSubSort A : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of b₃ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) * the ResultSort of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) . o : ( ( ) ( ) OperSymbol of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ;

definition

let S be ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ;
let U0 be ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;
let A be ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ;
assume A : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) is opers_closed ;

func U0 | A -> ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) equals :: MSUALG_2:def 15
MSAlgebra(# A : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) ,(Opers (U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ,A : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) )) : ( ( ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of (A : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ,A : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) * the ResultSort of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;

end;

definition

let S be ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ;
let U0 be ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;
let U1, U2 be ( ( ) ( ) MSSubAlgebra of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ;

func U1 /\ U2 -> ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) means :: MSUALG_2:def 16
( the Sorts of it : ( ( ) ( ) Element of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) = the Sorts of U1 : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) /\ the Sorts of U2 : ( ( ) ( ) Element of the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) & ( for B being ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) st B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) = the Sorts of it : ( ( ) ( ) Element of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) holds
( B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) is opers_closed & the Charact of it : ( ( ) ( ) Element of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of it : ( ( ) ( ) Element of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of it : ( ( ) ( ) Element of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) = Opers (U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ,B : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) : ( ( ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of (b₁ : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) #) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) * the Arity of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ,b₁ : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) * the ResultSort of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier' of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like ) set ) ) ) ) );

end;

definition

func GenMSAlg A -> ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) means :: MSUALG_2:def 17
( A : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) is ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of it : ( ( ) ( ) Element of the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) & ( for U1 being ( ( ) ( ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) st A : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) is ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U1 : ( ( ) ( ) MSSubAlgebra of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) holds
it : ( ( ) ( ) Element of the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) MSSubAlgebra of U1 : ( ( ) ( ) MSSubAlgebra of U0 : ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) ) );

end;

theorem :: MSUALG_2:21

theorem :: MSUALG_2:22

definition

let S be ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ;
let U0 be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;
let U1, U2 be ( ( ) ( ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ;

func U1 "\/" U2 -> ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) means :: MSUALG_2:def 18
for A being ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) st A : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) = the Sorts of U1 : ( ( V8() ) ( non empty Relation-like V8() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) \/ the Sorts of U2 : ( ( ) ( ) Element of the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) holds
it : ( ( ) ( ) Element of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) = GenMSAlg A : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) MSSubset of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ;

end;

theorem :: MSUALG_2:24

theorem :: MSUALG_2:27

for S being ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) )
for U1, U2 being ( ( ) ( ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) holds U1 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) /\ (U1 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) "\/" U2 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) : ( ( strict ) ( strict ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( strict ) ( strict ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) = MSAlgebra(# the Sorts of U1 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U1 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b₃ : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b₃ : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;

theorem :: MSUALG_2:28

for S being ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) )
for U1, U2 being ( ( ) ( ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) holds (U1 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) /\ U2 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ) : ( ( strict ) ( strict ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) "\/" U2 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( strict ) ( strict ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) = MSAlgebra(# the Sorts of U2 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U2 : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b₄ : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b₄ : ( ( ) ( ) MSSubAlgebra of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;

definition

func MSAlg_join U0 -> ( ( Function-like quasi_total ) ( non empty Relation-like [:(MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) set ) ,(MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) -valued Function-like V17([:(MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) set ) ,(MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) BinOp of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) means :: MSUALG_2:def 20
for x, y being ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) )
for U1, U2 being ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) st x : ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) = U1 : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) & y : ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) = U2 : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) holds
it : ( ( V8() ) ( non empty Relation-like V8() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) . (x : ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) = U1 : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) "\/" U2 : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ;

end;

definition

func MSAlg_meet U0 -> ( ( Function-like quasi_total ) ( non empty Relation-like [:(MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) set ) ,(MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) -valued Function-like V17([:(MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) set ) ,(MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ) quasi_total ) BinOp of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) means :: MSUALG_2:def 21
for x, y being ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) )
for U1, U2 being ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) st x : ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) = U1 : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) & y : ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) = U2 : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) holds
it : ( ( V8() ) ( non empty Relation-like V8() non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ManySortedSubset of the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) . (x : ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MSSub U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty ) set ) ) = U1 : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) /\ U2 : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( strict ) ( strict ) MSSubAlgebra of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ;

end;

theorem :: MSUALG_2:36

for S being ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign )
for U0 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) holds Top (MSSubAlLattice U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded ) Lattice) : ( ( ) ( ) Element of the carrier of (MSSubAlLattice b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = MSAlgebra(# the Sorts of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U0 : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b₂ : ( ( non-empty ) ( non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like non-empty non empty-yielding the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like non-empty non empty-yielding the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict non-empty ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ;

theorem :: MSUALG_2:37

for S being ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign )
for U0 being ( ( ) ( ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) holds MSAlgebra(# the Sorts of U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Charact of U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) V83() ) ManySortedFunction of the Arity of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ,( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) *) : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * ( the Sorts of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) #) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) )) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the ResultSort of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * the Sorts of b₂ : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( Relation-like ) ( non empty Relation-like non-empty non empty-yielding the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V17( the carrier' of b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) is ( ( ) ( ) MSSubAlgebra of U0 : ( ( ) ( ) MSAlgebra over b₁ : ( ( non empty non void ) ( non empty non void V60() ) ManySortedSign ) ) ) ;