theorem Th5: :: GLIB_001:6

for X being set
for fs being FinSequence of X
for fss being Subset of fs holds dom (Seq fss) = dom (Sgm (dom fss))