for I being set
for A, B being ManySortedSet of I
for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x