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