let R be non empty Poset; :: thesis: for A, B being OrderSortedSet of R
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" & F is order-sorted holds
F "" is order-sorted

let A, B be OrderSortedSet of R; :: thesis: for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" & F is order-sorted holds
F "" is order-sorted

let F be ManySortedFunction of A,B; :: thesis: ( F is "1-1" & F is "onto" & F is order-sorted implies F "" is order-sorted )
assume that
A1: F is "1-1" and
A2: F is "onto" and
A3: F is order-sorted ; :: thesis:
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: B . s1 c= B . s2 by ;
A6: (F "") . s2 = (F . s2) " by ;
A7: A . s1 c= A . s2 by ;
s1 in the carrier of R ;
then s1 in dom F by PARTFUN1:def 2;
then A8: F . s1 is one-to-one by ;
s2 in the carrier of R ;
then s2 in dom F by PARTFUN1:def 2;
then A9: F . s2 is one-to-one by ;
let a1 be set ; :: thesis: ( a1 in dom ((F "") . s1) implies ( a1 in dom ((F "") . s2) & ((F "") . s1) . a1 = ((F "") . s2) . a1 ) )
assume A10: a1 in dom ((F "") . s1) ; :: thesis: ( a1 in dom ((F "") . s2) & ((F "") . s1) . a1 = ((F "") . s2) . a1 )
A11: a1 in B . s1 by A10;
then A12: dom (F . s2) = A . s2 by ;
set c1 = ((F . s1) ") . a1;
set c2 = ((F . s2) ") . a1;
A13: dom (F . s1) = A . s1 by ;
A14: (F "") . s1 = (F . s1) " by ;
then A15: ((F . s1) ") . a1 in rng ((F . s1) ") by ;
A16: rng (F . s1) = B . s1 by ;
then (F . s1) " is Function of (B . s1),(A . s1) by ;
then A17: rng ((F . s1) ") c= A . s1 by RELAT_1:def 19;
then A18: ((F . s1) ") . a1 in A . s1 by A15;
A19: rng (F . s2) = B . s2 by ;
then A20: (F . s2) . (((F . s2) ") . a1) = a1 by
.= (F . s1) . (((F . s1) ") . a1) by
.= (F . s2) . (((F . s1) ") . a1) by A3, A4, A15, A17, A13 ;
a1 in B . s2 by ;
hence a1 in dom ((F "") . s2) by ; :: thesis: ((F "") . s1) . a1 = ((F "") . s2) . a1
(F . s2) " is Function of (B . s2),(A . s2) by ;
then ((F . s2) ") . a1 in dom (F . s2) by ;
hence ((F "") . s1) . a1 = ((F "") . s2) . a1 by ; :: thesis: verum