theorem Th4: :: EUCLID_2:4

for x being real-valued FinSequence holds |.x.| ^2 = |(x,x)|