theorem :: EUCLID_8:63

for p, q being Element of REAL 3 holds |(p,q)| = (((p . 1) * (q . 1)) + ((p . 2) * (q . 2))) + ((p . 3) * (q . 3)) by Lm5;