theorem :: EUCLID_4:15

for n being Nat
for x being Element of REAL n holds |.x.| = sqrt |(x,x)| ;