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 V2() ManySortedSubset of B st rngs F c= X holds
(G || X) ** F = G ** F