theorem Th6: :: MEASUR13:6

for n being non zero Nat
for X being non-empty b₁ + 1 -element FinSequence holds CarProduct X = [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):]