let m, n be non zero Nat; :: thesis: for X being non-empty m -element FinSequence st n < m holds
(ProdFinSeq X) . (n + 1) = [:((ProdFinSeq (SubFin (X,n))) . n),(ElmFin (X,(n + 1))):]
let X be non-empty m -element FinSequence; :: thesis: ( n < m implies (ProdFinSeq X) . (n + 1) = [:((ProdFinSeq (SubFin (X,n))) . n),(ElmFin (X,(n + 1))):] )
assume A1: n < m ; :: thesis: (ProdFinSeq X) . (n + 1) = [:((ProdFinSeq (SubFin (X,n))) . n),(ElmFin (X,(n + 1))):]
then A2: n + 1 <= m by NAT_1:13;
(ProdFinSeq X) . (n + 1) = [:((ProdFinSeq X) . n),(X . (n + 1)):] by A1, Def3
.= [:((ProdFinSeq (SubFin (X,n))) . n),(X . (n + 1)):] by A1, Th4 ;
hence (ProdFinSeq X) . (n + 1) = [:((ProdFinSeq (SubFin (X,n))) . n),(ElmFin (X,(n + 1))):] by A2, Def1; :: thesis: verum