let R be non empty Poset; :: thesis: for F being ManySortedFunction of the carrier of R st F is order-sorted holds
for s1, s2 being Element of R st s1 <= s2 holds
( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 )
let F be ManySortedFunction of the carrier of R; :: thesis: ( F is order-sorted implies for s1, s2 being Element of R st s1 <= s2 holds
( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 ) )
assume A1: F is order-sorted ; :: thesis: for s1, s2 being Element of R st s1 <= s2 holds
( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 )
let s1, s2 be Element of R; :: thesis: ( s1 <= s2 implies ( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 ) )
assume A2: s1 <= s2 ; :: thesis: ( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 )
thus dom (F . s1) c= dom (F . s2) by A1, A2; :: thesis: F . s1 c= F . s2
for a, b being object st [a,b] in F . s1 holds
[a,b] in F . s2

proof

let y, z be object ; :: thesis: ( [y,z] in F . s1 implies [y,z] in F . s2 )
assume A3: [y,z] in F . s1 ; :: thesis: [y,z] in F . s2
y in dom (F . s1) by A3, XTUPLE_0:def 12;
then A4: ( y in dom (F . s2) & (F . s1) . y = (F . s2) . y ) by A1, A2;
(F . s1) . y = z by A3, FUNCT_1:1;
hence [y,z] in F . s2 by A4, FUNCT_1:1; :: thesis: verum

end;

hence F . s1 c= F . s2 by RELAT_1:def 3; :: thesis: verum