for X1, X2 being natural-valued XFinSequence st len X1 = len X2 & ( for n being Nat st n in dom X1 holds
X1 . n <= X2 . n ) holds
Product X1 <= Product X2