theorem Th43: :: EUCLID_8:51

for p, q being Element of REAL 3 holds mlt (p,q) = <*((p . 1) * (q . 1)),((p . 2) * (q . 2)),((p . 3) * (q . 3))*>