theorem :: RFINSEQ:2

for f, g being FinSequence holds f ^ g,g ^ f are_fiberwise_equipotent