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 (Pt2FinSeq X) . m is Function of (CarProduct X),(product X) by Th7; :: thesis: verum