theorem :: GROUP_23:60

for I being non empty set
for F being Group-Family of I
for A being ManySortedSet of I st ( for i being Element of I holds A . i is Subset of (F . i) ) holds
product A is Subset of (product F)