theorem Th5: :: OSALG_3:5

for R being non empty Poset
for A being OrderSortedSet of R
for B, C being non-empty 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