theorem Th2: :: OSALG_3:2

for R being non empty Poset
for A being OrderSortedSet of R
for B being non-empty OrderSortedSet of R
for F being ManySortedFunction of A,B holds
( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds
for a1 being set st a1 in A . s1 holds
(F . s1) . a1 = (F . s2) . a1 )