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