for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B
for C, E being ManySortedSubset of A
for D being ManySortedSubset of C st E = D holds
(F || C) || D = F || E