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