for f, g being FinSequence
for m, n, j being Nat st f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Nat st 1 <= i & i <= m holds
f . i = g . i ) & ( for i being Nat st n < i & i <= len f holds
f . i = g . i ) & m < j & j <= n holds
ex k being Nat st
( m < k & k <= n & f . j = g . k )