theorem :: MSSUBFAM:15
for I being set
for F, G being ManySortedFunction of I holds G ** F is ManySortedFunction of I