theorem Th119: :: RVSUM_1:119
for x being real-valued FinSequence holds |(x,x)| >= 0