theorem Th7: :: MATRTOP1:7

for X being set
for f, f1 being FinSequence
for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q