let R be non empty Poset; :: thesis: for A, B being OrderSortedSet of
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 ; :: 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 A1: ( F is "1-1" & F is "onto" & 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 A2: 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 )
A3: ( B . s1 c= B . s2 & A . s1 c= A . s2 ) by A2, OSALG_1:def 18;
( s1 in the carrier of R & s2 in the carrier of R ) ;
then A4: ( s1 in dom F & s2 in dom F ) by PARTFUN1:def 4;
let a1 be set ; :: thesis: ( a1 in dom ((F "" ) . s1) implies ( a1 in dom ((F "" ) . s2) & ((F "" ) . s1) . a1 = ((F "" ) . s2) . a1 ) )
assume A5: a1 in dom ((F "" ) . s1) ; :: thesis: ( a1 in dom ((F "" ) . s2) & ((F "" ) . s1) . a1 = ((F "" ) . s2) . a1 )
A6: ( rng (F . s1) = B . s1 & rng (F . s2) = B . s2 ) by A1, MSUALG_3:def 3;
A7: ( F . s1 is one-to-one & F . s2 is one-to-one ) by A1, A4, MSUALG_3:def 2;
then A8: ( (F . s1) " is Function of (B . s1),(A . s1) & (F . s2) " is Function of (B . s2),(A . s2) ) by A6, FUNCT_2:31;
A9: ( (F "" ) . s1 = (F . s1) " & (F "" ) . s2 = (F . s2) " ) by A1, MSUALG_3:def 5;
A10: a1 in B . s1 by A5;
then A11: ( a1 in B . s2 & B . s2 <> {} ) by A3;
A12: ((F . s1) " ) . a1 in rng ((F . s1) " ) by A5, A9, FUNCT_1:12;
A13: rng ((F . s1) " ) c= A . s1 by A8, RELAT_1:def 19;
then A14: ( ((F . s1) " ) . a1 in A . s1 & A . s1 <> {} ) by A12;
hence a1 in dom ((F "" ) . s2) by A3, A11, FUNCT_2:def 1; :: thesis: ((F "" ) . s1) . a1 = ((F "" ) . s2) . a1
A15: ( dom (F . s1) = A . s1 & dom (F . s2) = A . s2 ) by A3, A10, FUNCT_2:def 1;
set c1 = ((F . s1) " ) . a1;
set c2 = ((F . s2) " ) . a1;
A16: ( ((F . s2) " ) . a1 in dom (F . s2) & ((F . s1) " ) . a1 in dom (F . s2) ) by A3, A8, A10, A14, A15, FUNCT_2:7;
(F . s2) . (((F . s2) " ) . a1) = a1 by A3, A6, A7, A10, FUNCT_1:57
.= (F . s1) . (((F . s1) " ) . a1) by A5, A6, A7, FUNCT_1:57
.= (F . s2) . (((F . s1) " ) . a1) by A1, A2, A12, A13, A15, Def1 ;
hence ((F "" ) . s1) . a1 = ((F "" ) . s2) . a1 by A7, A9, A16, FUNCT_1:def 8; :: thesis: verum