theorem :: MEASUR10:20

for X being non-empty 1 -element FinSequence
for S being FieldFamily of X holds SemiringProduct S is Field_Subset of (product X)