let R be non empty Poset; :: thesis: for F being ManySortedFunction of 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 ; :: thesis: ( 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 ; :: thesis: 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 * ; :: thesis: ( w1 <= w2 implies (F # ) . w1 c= (F # ) . w2 )
assume A2: w1 <= w2 ; :: thesis: (F # ) . w1 c= (F # ) . w2
A3: ( len w1 = len w2 & ( for i being set st i in dom w1 holds
for s1, s2 being Element of R st s1 = w1 . i & s2 = w2 . i holds
s1 <= s2 ) ) by A2, OSALG_1:def 7;
then A4: dom w1 = dom w2 by FINSEQ_3:31;
thus (F # ) . w1 c= (F # ) . w2 :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (F # ) . w1 or x in (F # ) . w2 )
assume A5: x in (F # ) . w1 ; :: thesis: x in (F # ) . w2
set a = (F # ) . w1;
set b = (F # ) . w2;
A6: ( (F # ) . w1 = product (F * w1) & (F # ) . w2 = product (F * w2) ) by PBOOLE:def 19;
then consider g being Function such that
A7: ( x = g & dom g = dom (F * w1) ) and
A8: for y being set st y in dom (F * w1) holds
g . y in (F * w1) . y by A5, CARD_3:def 5;
( w1 is FinSequence of the carrier of R & w2 is FinSequence of the carrier of R ) by FINSEQ_1:def 11;
then A9: ( rng w1 c= the carrier of R & rng w2 c= the carrier of R ) by RELAT_1:def 19;
dom F = the carrier of R by PARTFUN1:def 4;
then A10: ( dom (F * w1) = dom w1 & dom (F * w2) = dom w2 ) by A9, RELAT_1:46;
for z being set st z in dom (F * w2) holds
g . z in (F * w2) . z

proof

let z be set ; :: thesis: ( z in dom (F * w2) implies g . z in (F * w2) . z )
assume A11: z in dom (F * w2) ; :: thesis: g . z in (F * w2) . z
A12: z in dom (F * w1) by A3, A10, A11, FINSEQ_3:31;
A13: g . z in (F * w1) . z by A4, A8, A10, A11;
( w1 . z in rng w1 & w2 . z in rng w2 ) by A4, A10, A11, FUNCT_1:12;
then reconsider s1 = w1 . z, s2 = w2 . z as Element of R by A9;
A14: ( (F * w1) . z = F . (w1 . z) & (F * w2) . z = F . (w2 . z) ) by A4, A10, A11, FUNCT_1:22;
s1 <= s2 by A2, A10, A12, OSALG_1:def 7;
then F . s1 c= F . s2 by A1, Th2;
hence g . z in (F * w2) . z by A13, A14; :: thesis: verum

end;

hence x in (F # ) . w2 by A4, A6, A7, A10, CARD_3:def 5; :: thesis: verum

end;