theorem Th9: :: MATRTOP1:9

for X being set
for f, f1 being FinSubsequence
for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q