theorem Th31: :: RFINSEQ:31

for f, g, h being FinSequence holds
( f,g are_fiberwise_equipotent iff h ^ f,h ^ g are_fiberwise_equipotent )