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

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

hence
F . s1 c= F . s2
by RELAT_1:def 3; :: thesis: verum
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;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