theorem Th10: :: MESFUN18:10

for n being non zero Nat
for X, Y being b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
X . i c= Y . i ) holds
CarProduct X c= CarProduct Y