theorem Th11: :: MESFUN18:11

for n, k being non zero Nat
for X being non empty set
for D being b₁ -element FinSequence st k in Seg n & ( for i being Nat st i in Seg n holds
D . i is Subset of X ) holds
(ProdFinSeq D) . k is Subset of (CarProduct ((Seg k) --> X))