for f, g being FinSequence st f,g are_fiberwise_equipotent holds
( len f = len g & dom f = dom g )