for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for M1, M2 being ManySortedSubset of A st M1 c= M2 holds
(F || M2) .:.: M1 = F .:.: M1