let m, n be non zero Nat; :: thesis: for X being non-empty m -element FinSequence st n <= m holds
(ProdFinSeq X) . n = (ProdFinSeq (SubFin (X,n))) . n
let X be non-empty m -element FinSequence; :: thesis: ( n <= m implies (ProdFinSeq X) . n = (ProdFinSeq (SubFin (X,n))) . n )
assume A1: n <= m ; :: thesis: (ProdFinSeq X) . n = (ProdFinSeq (SubFin (X,n))) . n
len X = m by FINSEQ_3:153;
then X = X | m by FINSEQ_1:58;
then X = SubFin (X,m) by Def5;
hence (ProdFinSeq X) . n = (ProdFinSeq (SubFin (X,n))) . n by A1, Th3; :: thesis: verum