theorem Th17: :: MEASUR10:19

for X being non-empty 1 -element FinSequence
for S being FieldFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is Field_Subset of { <*x*> where x is Element of X . 1 : verum }