theorem :: MSSUBFAM:15

for I being set
for F, G being ManySortedFunction of I holds G ** F is ManySortedFunction of I