let R be non empty Poset; :: thesis: for F being ManySortedFunction of 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 ; :: 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) :: thesis: F . s1 c= F . s2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (F . s1) or x in dom (F . s2) )
assume A3: x in dom (F . s1) ; :: thesis: x in dom (F . s2)
thus x in dom (F . s2) by A1, A2, A3, Def1; :: thesis: verum

end;

for a, b being set st [a,b] in F . s1 holds
[a,b] in F . s2

proof

let y, z be set ; :: thesis: ( [y,z] in F . s1 implies [y,z] in F . s2 )
assume A4: [y,z] in F . s1 ; :: thesis: [y,z] in F . s2
y in dom (F . s1) by A4, RELAT_1:def 4;
then A5: ( y in dom (F . s2) & (F . s1) . y = (F . s2) . y ) by A1, A2, Def1;
(F . s1) . y = z by A4, FUNCT_1:8;
hence [y,z] in F . s2 by A5, FUNCT_1:8; :: thesis: verum

end;

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