theorem SH6: :: DBLSEQ_2:50

for X being non empty set
for s1, s2 being sequence of X
for n being Nat st s1,s2 are_fiberwise_equipotent holds
ex m being Nat ex fs2 being Subset of (Shift ((s2 | (Segm m)),1)) st Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent