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: 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: B . s1 c= B . s2 by A4, OSALG_1:def 16;

A6: (F "") . s2 = (F . s2) " by A1, A2, MSUALG_3:def 4;

A7: A . s1 c= A . s2 by A4, OSALG_1:def 16;

s1 in the carrier of R ;

then s1 in dom F by PARTFUN1:def 2;

then A8: F . s1 is one-to-one by A1, MSUALG_3:def 2;

s2 in the carrier of R ;

then s2 in dom F by PARTFUN1:def 2;

then A9: F . s2 is one-to-one by A1, MSUALG_3:def 2;

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 A5, FUNCT_2:def 1;

set c1 = ((F . s1) ") . a1;

set c2 = ((F . s2) ") . a1;

A13: dom (F . s1) = A . s1 by A10, FUNCT_2:def 1;

A14: (F "") . s1 = (F . s1) " by A1, A2, MSUALG_3:def 4;

then A15: ((F . s1) ") . a1 in rng ((F . s1) ") by A10, FUNCT_1:3;

A16: rng (F . s1) = B . s1 by A2, MSUALG_3:def 3;

then (F . s1) " is Function of (B . s1),(A . s1) by A8, FUNCT_2:25;

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 A2, MSUALG_3:def 3;

then A20: (F . s2) . (((F . s2) ") . a1) = a1 by A5, A9, A11, FUNCT_1:35

.= (F . s1) . (((F . s1) ") . a1) by A10, A16, A8, FUNCT_1:35

.= (F . s2) . (((F . s1) ") . a1) by A3, A4, A15, A17, A13 ;

a1 in B . s2 by A5, A11;

hence a1 in dom ((F "") . s2) by A7, A18, FUNCT_2:def 1; :: thesis: ((F "") . s1) . a1 = ((F "") . s2) . a1

(F . s2) " is Function of (B . s2),(A . s2) by A19, A9, FUNCT_2:25;

then ((F . s2) ") . a1 in dom (F . s2) by A5, A7, A11, A18, A12, FUNCT_2:5;

hence ((F "") . s1) . a1 = ((F "") . s2) . a1 by A7, A9, A14, A6, A18, A12, A20, FUNCT_1:def 4; :: thesis: verum

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: 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: B . s1 c= B . s2 by A4, OSALG_1:def 16;

A6: (F "") . s2 = (F . s2) " by A1, A2, MSUALG_3:def 4;

A7: A . s1 c= A . s2 by A4, OSALG_1:def 16;

s1 in the carrier of R ;

then s1 in dom F by PARTFUN1:def 2;

then A8: F . s1 is one-to-one by A1, MSUALG_3:def 2;

s2 in the carrier of R ;

then s2 in dom F by PARTFUN1:def 2;

then A9: F . s2 is one-to-one by A1, MSUALG_3:def 2;

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 A5, FUNCT_2:def 1;

set c1 = ((F . s1) ") . a1;

set c2 = ((F . s2) ") . a1;

A13: dom (F . s1) = A . s1 by A10, FUNCT_2:def 1;

A14: (F "") . s1 = (F . s1) " by A1, A2, MSUALG_3:def 4;

then A15: ((F . s1) ") . a1 in rng ((F . s1) ") by A10, FUNCT_1:3;

A16: rng (F . s1) = B . s1 by A2, MSUALG_3:def 3;

then (F . s1) " is Function of (B . s1),(A . s1) by A8, FUNCT_2:25;

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 A2, MSUALG_3:def 3;

then A20: (F . s2) . (((F . s2) ") . a1) = a1 by A5, A9, A11, FUNCT_1:35

.= (F . s1) . (((F . s1) ") . a1) by A10, A16, A8, FUNCT_1:35

.= (F . s2) . (((F . s1) ") . a1) by A3, A4, A15, A17, A13 ;

a1 in B . s2 by A5, A11;

hence a1 in dom ((F "") . s2) by A7, A18, FUNCT_2:def 1; :: thesis: ((F "") . s1) . a1 = ((F "") . s2) . a1

(F . s2) " is Function of (B . s2),(A . s2) by A19, A9, FUNCT_2:25;

then ((F . s2) ") . a1 in dom (F . s2) by A5, A7, A11, A18, A12, FUNCT_2:5;

hence ((F "") . s1) . a1 = ((F "") . s2) . a1 by A7, A9, A14, A6, A18, A12, A20, FUNCT_1:def 4; :: thesis: verum