let R be non empty Poset; :: thesis: 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; :: 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 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

set a = (F # ) . w1;
set b = (F # ) . w2;
A5: (F # ) . w1 = product (F * w1) by PBOOLE:def 19;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (F # ) . w1 or x in (F # ) . w2 )
assume x in (F # ) . w1 ; :: thesis: x in (F # ) . w2
then consider g being Function such that
A6: ( x = g & dom g = dom (F * w1) ) and
A7: for y being set 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 4;
w2 is FinSequence of the carrier of R by FINSEQ_1:def 11;
then A9: rng w2 c= the carrier of R by RELAT_1:def 19;
then A10: dom (F * w2) = dom w2 by A8, RELAT_1:46;
w1 is FinSequence of the carrier of R by FINSEQ_1:def 11;
then A11: rng w1 c= the carrier of R by RELAT_1:def 19;
then A12: dom (F * w1) = dom w1 by A8, RELAT_1:46;
A13: 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 A14: z in dom (F * w2) ; :: thesis: g . z in (F * w2) . z
A15: (F * w2) . z = F . (w2 . z) by A14, FUNCT_1:22;
( w1 . z in rng w1 & w2 . z in rng w2 ) by A4, A10, A14, FUNCT_1:12;
then reconsider s1 = w1 . z, s2 = w2 . z as Element of R by A11, A9;
z in dom (F * w1) by A3, A12, A10, A14, FINSEQ_3:31;
then s1 <= s2 by A2, A12, OSALG_1:def 7;
then A16: F . s1 c= F . s2 by A1, Th2;
( g . z in (F * w1) . z & (F * w1) . z = F . (w1 . z) ) by A4, A7, A12, A10, A14, FUNCT_1:22;
hence g . z in (F * w2) . z by A15, A16; :: thesis: verum

end;

(F # ) . w2 = product (F * w2) by PBOOLE:def 19;
hence x in (F # ) . w2 by A4, A6, A12, A10, A13, CARD_3:def 5; :: thesis: verum

end;