let R be non empty Poset; :: thesis: 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 )
let A be OrderSortedSet of R; :: thesis: 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 )
let B be non-empty OrderSortedSet of R; :: thesis: 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 )
let F be ManySortedFunction of A,B; :: thesis: ( 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 )

hereby :: thesis: ( ( 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 ) implies F is order-sorted )

assume A1: F is order-sorted ; :: thesis: 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
let s1, s2 be Element of R; :: thesis: ( s1 <= s2 implies for a1 being set st a1 in A . s1 holds
(F . s1) . a1 = (F . s2) . a1 )
assume A2: s1 <= s2 ; :: thesis: for a1 being set st a1 in A . s1 holds
(F . s1) . a1 = (F . s2) . a1
let a1 be set ; :: thesis: ( a1 in A . s1 implies (F . s1) . a1 = (F . s2) . a1 )
assume a1 in A . s1 ; :: thesis: (F . s1) . a1 = (F . s2) . a1
then a1 in dom (F . s1) by FUNCT_2:def 1;
hence (F . s1) . a1 = (F . s2) . a1 by A1, A2; :: thesis: verum

end;

assume A3: 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 ; :: thesis: F is order-sorted
let s1, s2 be Element of R; :: according to OSALG_3:def 1 :: thesis: ( s1 <= s2 implies for a1 being set st a1 in dom (F . s1) holds
( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) )
assume A4: s1 <= s2 ; :: thesis: for a1 being set st a1 in dom (F . s1) holds
( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 )
A5: ( dom (F . s1) = A . s1 & dom (F . s2) = A . s2 ) by FUNCT_2:def 1;
let a1 be set ; :: thesis: ( a1 in dom (F . s1) implies ( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) )
assume A6: a1 in dom (F . s1) ; :: thesis: ( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 )
A . s1 c= A . s2 by A4, OSALG_1:def 16;
hence a1 in dom (F . s2) by A6, A5; :: thesis: (F . s1) . a1 = (F . s2) . a1
thus (F . s1) . a1 = (F . s2) . a1 by A3, A4, A6; :: thesis: verum