let R be non empty Poset; 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; 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; ( 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
; F "" is order-sorted
let s1, s2 be Element of R; OSALG_3:def 1 ( 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
; 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 ; ( a1 in dom ((F "") . s1) implies ( a1 in dom ((F "") . s2) & ((F "") . s1) . a1 = ((F "") . s2) . a1 ) )
assume A10:
a1 in dom ((F "") . s1)
; ( 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; ((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; verum