let m, n, k be non zero Nat; :: thesis: for X being non-empty m -element FinSequence st k <= n & n <= m holds
(Pt2FinSeq X) . k = (Pt2FinSeq (SubFin (X,n))) . k
let X be non-empty m -element FinSequence; :: thesis: ( k <= n & n <= m implies (Pt2FinSeq X) . k = (Pt2FinSeq (SubFin (X,n))) . k )
assume A1: ( k <= n & n <= m ) ; :: thesis: (Pt2FinSeq X) . k = (Pt2FinSeq (SubFin (X,n))) . k
A2: len X = m by FINSEQ_3:153;
SubFin (X,m) = X | m by MEASUR13:def 5;
then SubFin (X,m) = X by A2, FINSEQ_1:58;
hence (Pt2FinSeq X) . k = (Pt2FinSeq (SubFin (X,n))) . k by A1, Th9; :: thesis: verum