theorem Th4: :: MESFUN18:4

for n being non zero Nat
for D being b₁ + 1 -element FinSequence
for D1 being b₁ -element FinSequence st D1 = D | n holds
CarProduct D = [:(CarProduct D1),(D . (n + 1)):]