let m be non zero Nat; :: thesis: for X being non-empty m -element FinSequence holds CarProd X is bijective
let X be non-empty m -element FinSequence; :: thesis: CarProd X is bijective
A1: len X = m by FINSEQ_3:153;
SubFin (X,m) = X | m by MEASUR13:def 5;
then SubFin (X,m) = X by A1, FINSEQ_1:58;
hence CarProd X is bijective by Th11; :: thesis: verum