theorem :: NUMBER11:11

for d1, d2 being XFinSequence of NAT
for b being Nat st b > 1 & dom d1 = dom d2 & ( for n being Nat st n in dom d1 holds
d1 . n <= d2 . n ) holds
value (d1,b) <= value (d2,b)