theorem :: HILB10_4:11

for i being Nat
for X being natural-valued positive-yielding XFinSequence st i in dom X holds
X . i <= Product X