theorem Th2: :: SRINGS_5:2
for n being Nat
for x being Element of REAL n
for i being Nat st i in Seg n holds
(abs x) . i in REAL