let p, q be Element of REAL 3; :: thesis: mlt (p,q) = <*((p . 1) * (q . 1)),((p . 2) * (q . 2)),((p . 3) * (q . 3))*>
( len p = 3 & len q = 3 ) by Th42;
hence mlt (p,q) = <*((p . 1) * (q . 1)),((p . 2) * (q . 2)),((p . 3) * (q . 3))*> by EUCLID_5:28; :: thesis: verum