for f, g being FinSequence of INT
for m, n being Nat st 1 <= n & n <= len f & 1 <= m & m <= len f & len f = len g & f . m = g . n & f . n = g . m & ( for k being Nat st k <> m & k <> n & 1 <= k & k <= len f holds
f . k = g . k ) holds
f,g are_fiberwise_equipotent