theorem Th1: :: RFINSEQ:1

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