theorem Th9: :: MEASUR13:9

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