let R be non empty Poset; :: thesis: for A being OrderSortedSet of
for B being V5() OrderSortedSet of
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 ; :: thesis: for B being V5() OrderSortedSet of
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 V5() OrderSortedSet of ; :: 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 A3: a1 in A . s1 ; :: thesis: (F . s1) . a1 = (F . s2) . a1
a1 in dom (F . s1) by A3, FUNCT_2:def 1;
hence (F . s1) . a1 = (F . s2) . a1 by A1, A2, Def1; :: thesis: verum

end;

assume A4: 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 A5: 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 )
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 )
A7: A . s1 c= A . s2 by A5, OSALG_1:def 18;
( dom (F . s1) = A . s1 & dom (F . s2) = A . s2 ) by FUNCT_2:def 1;
hence a1 in dom (F . s2) by A6, A7; :: thesis: (F . s1) . a1 = (F . s2) . a1
thus (F . s1) . a1 = (F . s2) . a1 by A4, A5, A6; :: thesis: verum