for O being set
for f1, f2 being FinSequence
for i, j being Nat st i in dom f1 & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p ") . i ) holds
ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O