let R be non empty Poset; for F being ManySortedFunction of the carrier of R st F is order-sorted holds
for w1, w2 being Element of the carrier of R * st w1 <= w2 holds
(F #) . w1 c= (F #) . w2
let F be ManySortedFunction of the carrier of R; ( F is order-sorted implies for w1, w2 being Element of the carrier of R * st w1 <= w2 holds
(F #) . w1 c= (F #) . w2 )
assume A1:
F is order-sorted
; for w1, w2 being Element of the carrier of R * st w1 <= w2 holds
(F #) . w1 c= (F #) . w2
let w1, w2 be Element of the carrier of R * ; ( w1 <= w2 implies (F #) . w1 c= (F #) . w2 )
assume A2:
w1 <= w2
; (F #) . w1 c= (F #) . w2
A3:
len w1 = len w2
by A2;
then A4:
dom w1 = dom w2
by FINSEQ_3:29;
thus
(F #) . w1 c= (F #) . w2
verumproof
set a =
(F #) . w1;
set b =
(F #) . w2;
A5:
(F #) . w1 = product (F * w1)
by FINSEQ_2:def 5;
let x be
object ;
TARSKI:def 3 ( not x in (F #) . w1 or x in (F #) . w2 )
assume
x in (F #) . w1
;
x in (F #) . w2
then consider g being
Function such that A6:
(
x = g &
dom g = dom (F * w1) )
and A7:
for
y being
object st
y in dom (F * w1) holds
g . y in (F * w1) . y
by A5, CARD_3:def 5;
A8:
dom F = the
carrier of
R
by PARTFUN1:def 2;
rng w2 c= the
carrier of
R
;
then A9:
dom (F * w2) = dom w2
by A8, RELAT_1:27;
rng w1 c= the
carrier of
R
;
then A10:
dom (F * w1) = dom w1
by A8, RELAT_1:27;
A11:
for
z being
object st
z in dom (F * w2) holds
g . z in (F * w2) . z
proof
let z be
object ;
( z in dom (F * w2) implies g . z in (F * w2) . z )
assume A12:
z in dom (F * w2)
;
g . z in (F * w2) . z
A13:
(F * w2) . z = F . (w2 . z)
by A12, FUNCT_1:12;
(
w1 . z in rng w1 &
w2 . z in rng w2 )
by A4, A9, A12, FUNCT_1:3;
then reconsider s1 =
w1 . z,
s2 =
w2 . z as
Element of
R ;
z in dom (F * w1)
by A3, A10, A9, A12, FINSEQ_3:29;
then
s1 <= s2
by A2, A10;
then A14:
F . s1 c= F . s2
by A1, Th1;
(
g . z in (F * w1) . z &
(F * w1) . z = F . (w1 . z) )
by A4, A7, A10, A9, A12, FUNCT_1:12;
hence
g . z in (F * w2) . z
by A13, A14;
verum
end;
(F #) . w2 = product (F * w2)
by FINSEQ_2:def 5;
hence
x in (F #) . w2
by A4, A6, A10, A9, A11, CARD_3:def 5;
verum
end;