:: deftheorem defines order-sorted OSALG_3:def 1 :
for R being non empty Poset
for F being ManySortedFunction of the carrier of R holds
( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds
for a1 being set st a1 in dom (F . s1) holds
( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) );