theorem Th4: :: RFINSEQ:4

for f, g being FinSequence holds
( f,g are_fiberwise_equipotent iff ex P being Permutation of (dom g) st f = g * P )