theorem :: MEASUR13:11

for n, i being non zero Nat
for X being non-empty b₁ + 1 -element FinSequence
for S being sigmaFieldFamily of X st i <= n holds
CarProduct (SubFin (X,i)) = CarProduct (SubFin ((SubFin (X,n)),i))