for R being non empty Poset
for A being OrderSortedSet of R
for B, C being V2() OrderSortedSet of R
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is order-sorted & G is order-sorted holds
G ** F is order-sorted