for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X)