theorem Th8: :: MESFUN18:8

for n being non zero Nat
for D being b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is Element of L-Field ) holds
CarProduct D is Element of Prod_Field (L-Field n)