theorem SH7: :: DBLSEQ_2:51

for X being non empty set
for fs being FinSequence of X
for fss being Subset of fs holds Seq fss,fss are_fiberwise_equipotent