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;
then A4: dom w1 = dom w2 by FINSEQ_3:29;
thus (F #) . w1 c= (F #) . w2 :: thesis: verum

proof

set a = (F #) . w1;
set b = (F #) . w2;
A5: (F #) . w1 = product (F * w1) by FINSEQ_2:def 5;
let x be object ; :: 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 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 ; :: thesis: ( z in dom (F * w2) implies g . z in (F * w2) . z )
assume A12: z in dom (F * w2) ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;