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 Th35;
hence mlt p,q = <*((p . 1) * (q . 1)),((p . 2) * (q . 2)),((p . 3) * (q . 3))*> by EUCLID_5:28; :: thesis: verum